bluuebunny/crossref_metadata_2025_split huggingface dataset:
Effectiveness of foot orthoses and shock-absorbing insoles for the prevention of injury: a systematic review and meta-analysis
Authors: Bonanno Daniel R , Landorf Karl B , Munteanu Shannon E , Murley George S , Menz Hylton B 
Published: December 2016

ObjectiveTo investigate the evidence relating to the effectiveness of foot orthoses and shock-absorbing insoles for the prevention of musculoskeletal injury.DesignSystematic review and meta-analysis.Eligibility criteria for selecting studiesClinical trials evaluating the effectiveness of foot orthoses and shock-absorbing insoles for the prevention of injury.Data sourcesCochrane Library, CINAHL, EMBASE, MEDLINE and SPORTDiscus from their inception up to the first week of June 2016.Results11 trials that had evaluated foot orthoses and 7 trials that had evaluated shock-absorbing insoles were included. The median Physiotherapy Evidence Database (PEDro) score for trials that had evaluated foot orthoses and shock-absorbing insoles was 5 (range 3–8/10) and 3 (range 1–7/10), respectively. Meta-analysis found that foot orthoses were effective for preventing overall injuries (risk ratio (RR) 0.72, 95% CI 0.55 to 0.94) and stress fractures (RR 0.59, 95% CI 0.45 to 0.76), but not soft-tissue injuries (RR 0.79, 95% CI 0.55 to 1.14). In contrast, shock-absorbing insoles were not effective for preventing overall injuries (RR 0.92, 95% CI 0.73 to 1.16), stress fractures (RR 1.15, 95% CI 0.57 to 2.32) or soft-tissue injuries (RR 0.92, 95% CI 0.74 to 1.15).ConclusionsFoot orthoses were found to be effective for preventing overall injuries and stress fractures but not soft-tissue injuries, while shock-absorbing insoles were not found to be effective for preventing any injury. However, further well-designed trials will assist the accuracy and precision of the estimates of risk reduction as the quality of the included trials varied greatly.
Caffeine consumption during pregnancy and ADHD at the age of 11 years: a birth cohort study
Authors: Del-Ponte Bianca , Santos Iná S , Tovo-Rodrigues Luciana , Anselmi Luciana , Munhoz Tiago N , Matijasevich Alicia 
Published: December 2016

ObjectiveStudies evaluating caffeine intake during pregnancy and long-term outcomes, such as the child's neurobehaviour, are still scarce and their results are inconsistent. The objective of the present study was to evaluate the association between maternal consumption of caffeine during pregnancy and attention deficit hyperactivity disorder (ADHD) at the age of 11 years.MethodologyAll children born in the city of Pelotas, Brazil, during the year 2004, were selected for a cohort study. The mothers were interviewed at birth to obtain information on coffee and yerba mate consumption during pregnancy, among other matters. At the age of 11 years, presence of ADHD was evaluated using the Development and Well-Being Assessment (DAWBA) questionnaire, applied to the mothers. The prevalence of ADHD was calculated, with 95% CIs. The association between caffeine consumption and ADHD was tested by means of logistic regression.Results3485 children were included in the analyses. The prevalence of ADHD was 4.1% (95% CI 3.4% to 4.7%): 5.8% (95% CI 4.7% to 6.9%) among boys and 2.3% (95% CI 1.5% to 3.0%) among girls. The prevalence of caffeine consumption during the entire pregnancy and in the first, second and third trimesters was 88.7% (87.7% to 89.7%), 86.5% (85.4% to 87.5%), 83.0% (81.8% to 84.2%) and 92.3% (91.4% to 93.1%), respectively. Caffeine consumption during the entire pregnancy and the first, second and third trimesters were not associated with ADHD in the crude or adjusted analysis.ConclusionsThe present study did not show any association between maternal caffeine consumption during pregnancy and ADHD at the age of 11 years.
Quality of prescribing of antipsychotic medication for people with intellectual disability under the care of UK mental health services: a cross-sectional audit of clinical practice
Authors: Paton Carol , Bhatti Sumera , Purandare Kiran , Roy Ashok , Barnes TRE 
Published: December 2016

ObjectivesTo determine the prevalence and quality of antipsychotic prescribing for people with intellectual disability (ID).DesignA clinical audit of prescribing practice in the context of a quality improvement programme. Practice standards for audit were derived from relevant, evidence-based guidelines, including NICE. Data were mainly collected from the clinical records, but to determine the clinical rationale for using antipsychotic medication in individual cases, prescribers could also be directly questioned.Settings54 mental health services in the UK, which were predominantly NHS Trusts.ParticipantsInformation on prescribing was collected for 5654 people with ID.ResultsAlmost two-thirds (64%) of the total sample was prescribed antipsychotic medication, of whom almost half (49%) had a schizophrenia spectrum or affective disorder diagnosis, while a further third (36%) exhibited behaviours recognised by NICE as potentially legitimate targets for such treatment such as violence, aggression or self-injury. With respect to screening for potential side effects within the past year, 41% had a documented measure of body weight (range across participating services 18–100%), 32% blood pressure (0–100%) and 37% blood glucose and blood lipids (0–100%).ConclusionsThese data from mental health services across the UK suggest that antipsychotic medications are not widely used outside of licensed and/or evidence-based indications in people with ID. However, screening for side effects in those patients on continuing antipsychotic medication was inconsistent across the participating services and the possibility that a small number of these services failed to meet basic standards of care cannot be excluded.
Managing complex respiratory patients in the community: an evaluation of a pilot integrated respiratory care service
Authors: Gillett K , Lippiett K , Astles C , Longstaff J , Orlando R , Lin S X , Powell A , Roberts C , Chauhan A J , Thomas M , Wilkinson T M 
Published: December 2016

IntroductionIn the UK, there is significant variation in respiratory care and outcomes. An integrated approach to the management of high-risk respiratory patients, incorporating specialist and primary care teams' expertise, is the basis for new integrated respiratory services designed to reduce this variation; however, this model needs evaluating.MethodsTo evaluate an integrated service managing high-risk respiratory patients, electronic searches for patients with asthma and chronic obstructive pulmonary disease at risk of poor outcomes were performed in two general practitioner (GP) practices in a local service-development initiative. Patients were reviewed at joint clinics by primary and secondary care professionals. GPs also nominated patients for inclusion. Reviews were delivered to best standards of care including assessments of diagnosis, control, spirometry, self-management, education, medication, inhaler technique and smoking cessation support. Follow-up of routine clinical data collected at 9-months postclinic were compared with seasonally matched 9-months prior to integrated review.Results82 patients were identified, 55 attended. 13 (23.6%) had their primary diagnosis changed. In comparison with the seasonally adjusted baseline period, in the 9-month follow-up there was an increase in inhaled corticosteroid prescriptions of 23.3%, a reduction in short-acting β2-agonist prescription of 33.3%, a reduction in acute respiratory exacerbations of 67.6%, in unscheduled GP surgery visits of 53.3% and acute respiratory hospital admissions reduced from 3 to 0. Only 4 patients (7.3%) required referral to secondary care. Health economic evaluation showed respiratory-related costs per patient reduced by £231.86.ConclusionsPatients with respiratory disease in this region at risk of suboptimal outcomes identified proactively and managed by an integrated team improved outcomes without the need for hospital referral.
Clinical relevance of pharmacist intervention in an emergency department
Authors: Pérez-Moreno Maria Antonia , Rodríguez-Camacho Juan Manuel , Calderón-Hernanz Beatriz , Comas-Díaz Bernardino , Tarradas-Torras Jordi 
Published: December 2016

ObjectivesTo evaluate the clinical relevance of pharmacist intervention on patient care in emergencies, to determine the severity of detected errors. Second, to analyse the most frequent types of interventions and type of drugs involved and to evaluate the clinical pharmacist's activity.MethodsA 6-month observational prospective study of pharmacist intervention in the Emergency Department (ED) at a 400-bed hospital in Spain was performed to record interventions carried out by the clinical pharmacists. We determined whether the intervention occurred in the process of medication reconciliation or another activity, and whether the drug involved belonged to the High-Alert Medications Institute for Safe Medication Practices (ISMP) list. To evaluate the severity of the errors detected and clinical relevance of the pharmacist intervention, a modified assessment scale of Overhage and Lukes was used. Relationship between clinical relevance of pharmacist intervention and the severity of medication errors was assessed using ORs and Spearman's correlation coefficient.ResultsDuring the observation period, pharmacists reviewed the pharmacotherapy history and medication orders of 2984 patients. A total of 991 interventions were recorded in 557 patients; 67.2% of the errors were detected during medication reconciliation. Medication errors were considered severe in 57.2% of cases and 64.9% of pharmacist intervention were considered relevant. About 10.9% of the drugs involved are in the High-Alert Medications ISMP list. The severity of the medication error and the clinical significance of the pharmacist intervention were correlated (Spearman's ρ=0.728/p<0.001).ConclusionsIn this single centre study, the clinical pharmacists identified and intervened on a high number of severe medication errors. This suggests that emergency services will benefit from pharmacist-provided drug therapy services.
Vascular angular remodeling by kissing-Y stenting in wide necked intracranial bifurcation aneurysms
Authors: Melber Katharina , Meila Dan , Draheim Philipp , Grieb Dominik , Greling Björn , Schlunz-Hendann Martin , Brassel Friedhelm 
Published: December 2016

IntroductionSingle stent deployment leads to a change in vascular geometry in wide necked bifurcation aneurysms. In some complex cases, the use of the single stent technique might not be sufficient or may not be feasible. The kissing-Y stenting technique appears to be an alternative endovascular treatment option. The aim of this study was to evaluate the effects of the kissing-Y stenting technique on vascular angular remodeling.Methods21 patients with wide necked intracranial bifurcation aneurysms at different sites (10 anterior communicating artery, 6 middle cerebral artery, 3 basilar artery, 1 vertebral artery/posterior inferior cerebellar artery, 1 internal carotid artery/posterior communicating artery) were treated with 44 closed cell stents (follow-up 2012–2016) using the kissing-Y stenting technique. We analyzed vascular angle geometry between the mother and both affected daughter vessels by digital subtraction angiography, before and after stent deployment, using standard working projections.ResultsEndovascular treatment of wide necked intracranial aneurysms using the kissing-Y stenting technique significantly decreased the angle between the bifurcation branches from 130.4±9.5° to 91.5±9.1° (p<0.0001).ConclusionsKissing-Y stenting in wide necked bifurcation aneurysms leads to vascular angular remodeling of both affected branches. The resulting straightening of the bifurcation angle may prevent aneurysmal recurrence.
Talking bananas: structural recursion for session types
Authors: Lindley Sam , Morris J. Garrett 
Published: December 2016

Session types provide static guarantees that concurrent programs respect communication protocols. We give a novel account of recursive session types in the context of GV, a small concurrent extension of the linear λ-calculus. We extend GV with recursive types and catamorphisms, following the initial algebra semantics of recursion, and show that doing so naturally gives rise to recursive session types. We show that this principled approach to recursion resolves long-standing problems in the treatment of duality for recursive session types.
We characterize the expressiveness of GV concurrency by giving a CPS translation to (non-concurrent) λ-calculus and proving that reduction in GV is simulated by full reduction in λ-calculus. This shows that GV remains terminating in the presence of positive recursive types, and that such arguments extend to other extensions of GV, such as polymorphism or non-linear types, by appeal to normalization results for sequential λ-calculi. We also show that GV remains deadlock free and deterministic in the presence of recursive types.
Finally, we extend CP, a session-typed process calculus based on linear logic, with recursive types, and show that doing so preserves the connection between reduction in GV and cut elimination in CP.
A new verified compiler backend for CakeML
Authors: Tan Yong Kiam , Myreen Magnus O. , Kumar Ramana , Fox Anthony , Owens Scott , Norrish Michael 
Published: December 2016

We have developed and mechanically verified a new compiler backend for CakeML. Our new compiler features a sequence of intermediate languages that allows it to incrementally compile away high-level features and enables verification at the right levels of semantic detail. In this way, it resembles mainstream (unverified) compilers for strict functional languages. The compiler supports efficient curried multi-argument functions, configurable data representations, exceptions that unwind the call stack, register allocation, and more. The compiler targets several architectures: x86-64, ARMv6, ARMv8, MIPS-64, and RISC-V.
In this paper, we present the overall structure of the compiler, including its 12 intermediate languages, and explain how everything fits together. We focus particularly on the interaction between the verification of the register allocator and the garbage collector, and memory representations. The entire development has been carried out within the HOL4 theorem prover.
Experience report: growing and shrinking polygons for random testing of computational geometry algorithms
Authors: Sergey Ilya 
Published: December 2016

This paper documents our experience of adapting and using the QuickCheck-style approach for extensive randomised property-based testing of computational geometry algorithms.
The need in rigorous evaluation of computational geometry procedures has naturally arisen in our quest of organising a medium-size programming contest for second year university students—an experiment we conducted as an attempt to introduce them to computational geometry. The main effort in organising the event was implementation of a solid infrastructure for testing and ranking solutions. For this, we employed functional programming techniques. The choice of the language and the paradigm made it possible for us to engineer, from scratch and in a very short period of time, a series of robust geometric primitives and algorithms, as well as implement a scalable framework for their randomised testing.
We describe the main insights, enabling efficient random testing of geometric procedures, and report on our experience of using the testing framework, which helped us to detect and fix a number of issues not just in our programming artefacts, but also in the published algorithms we had implemented.
Set-theoretic types for polymorphic variants
Authors: Castagna Giuseppe , Petrucciani Tommaso , Nguyễn Kim 
Published: December 2016

Polymorphic variants are a useful feature of the OCaml language whose current definition and implementation rely on kinding constraints to simulate a subtyping relation via unification. This yields an awkward formalization and results in a type system whose behaviour is in some cases unintuitive and/or unduly restrictive.
In this work, we present an alternative formalization of polymorphic variants, based on set-theoretic types and subtyping, that yields a cleaner and more streamlined system. Our formalization is more expressive than the current one (it types more programs while preserving type safety), it can internalize some meta-theoretic properties, and it removes some pathological cases of the current implementation resulting in a more intuitive and, thus, predictable type system. More generally, this work shows how to add full-fledged union types to functional languages of the ML family that usually rely on the Hindley-Milner type system. As an aside, our system also improves the theory of semantic subtyping, notably by proving completeness for the type reconstruction algorithm.
Indexed codata types
Authors: Thibodeau David , Cave Andrew , Pientka Brigitte 
Published: December 2016

Indexed data types allow us to specify and verify many interesting invariants about finite data in a general purpose programming language. In this paper we investigate the dual idea: indexed codata types, which allow us to describe data-dependencies about infinite data structures. Unlike finite data which is defined by constructors, we define infinite data by observations. Dual to pattern matching on indexed data which may refine the type indices, we define copattern matching on indexed codata where type indices guard observations we can make.
Our key technical contributions are three-fold: first, we extend Levy's call-by-push value language with support for indexed (co)data and deep (co)pattern matching; second, we provide a clean foundation for dependent (co)pattern matching using equality constraints; third, we describe a small-step semantics using a continuation-based abstract machine, define coverage for indexed (co)patterns, and prove type safety. This is an important step towards building a foundation where (co)data type definitions and dependent types can coexist.
Oh Lord, please don't let contracts be misunderstood (functional pearl)
Authors: Dimoulas Christos , New Max S. , Findler Robert Bruce , Felleisen Matthias 
Published: December 2016

Contracts feel misunderstood, especially those with a higher-order soul. While software engineers appreciate contracts as tools for articulating the interface between components, functional programmers desperately search for their types and meaning, completely forgetting about their pragmatics.
This gem presents a novel analysis of contract systems. Applied to the higher-order kind, this analysis reveals their large and clearly unappreciated software engineering potential. Three sample applications illustrate where this kind of exploration may lead.
Hierarchical memory management for parallel programs
Authors: Raghunathan Ram , Muller Stefan K. , Acar Umut A. , Blelloch Guy 
Published: December 2016

An important feature of functional programs is that they are parallel by default. Implementing an efficient parallel functional language, however, is a major challenge, in part because the high rate of allocation and freeing associated with functional programs requires an efficient and scalable memory manager.
In this paper, we present a technique for parallel memory management for strict functional languages with nested parallelism. At the highest level of abstraction, the approach consists of a technique to organize memory as a hierarchy of heaps, and an algorithm for performing automatic memory reclamation by taking advantage of a disentanglement property of parallel functional programs. More specifically, the idea is to assign to each parallel task its own heap in memory and organize the heaps in a hierarchy/tree that mirrors the hierarchy of tasks.
We present a nested-parallel calculus that specifies hierarchical heaps and prove in this calculus a disentanglement property, which prohibits a task from accessing objects allocated by another task that might execute in parallel. Leveraging the disentanglement property, we present a garbage collection technique that can operate on any subtree in the memory hierarchy concurrently as other tasks (and/or other collections) proceed in parallel. We prove the safety of this collector by formalizing it in the context of our parallel calculus. In addition, we describe how the proposed techniques can be implemented on modern shared-memory machines and present a prototype implementation as an extension to MLton, a high-performance compiler for the Standard ML language. Finally, we evaluate the performance of this implementation on a number of parallel benchmarks.
Allocation characterizes polyvariance: a unified methodology for polyvariant control-flow analysis
Authors: Gilray Thomas , Adams Michael D. , Might Matthew 
Published: December 2016

The polyvariance of a static analysis is the degree to which it structurally differentiates approximations of program values. Polyvariant techniques come in a number of different flavors that represent alternative heuristics for managing the trade-off an analysis strikes between precision and complexity. For example, call sensitivity supposes that values will tend to correlate with recent call sites, object sensitivity supposes that values will correlate with the allocation points of related objects, the Cartesian product algorithm supposes correlations between the values of arguments to the same function, and so forth.
In this paper, we describe a unified methodology for implementing and understanding polyvariance in a higher-order setting (i.e., for control-flow analyses). We do this by extending the method of abstracting abstract machines (AAM), a systematic approach to producing an abstract interpretation of abstract-machine semantics. AAM eliminates recursion within a language’s semantics by passing around an explicit store, and thus places importance on the strategy an analysis uses for allocating abstract addresses within the abstract heap or store. We build on AAM by showing that the design space of possible abstract allocators exactly and uniquely corresponds to the design space of polyvariant strategies. This allows us to both unify and generalize polyvariance as tunings of a single function. Changes to the behavior of this function easily recapitulate classic styles of analysis and produce novel variations, combinations of techniques, and fundamentally new techniques.
A lambda-calculus foundation for universal probabilistic programming
Authors: Borgström Johannes , Dal Lago Ugo , Gordon Andrew D. , Szymczak Marcin 
Published: December 2016

We develop the operational semantics of an untyped probabilistic λ-calculus with continuous distributions, and both hard and soft constraints,as a foundation for universal probabilistic programming languages such as Church, Anglican, and Venture. Our first contribution is to adapt the classic operational semantics of λ-calculus to a continuous setting via creating a measure space on terms and defining step-indexed approximations. We prove equivalence of big-step and small-step formulations of this
distribution-based semantics
. To move closer to inference techniques, we also define the
sampling-based semantics
of a term as a function from a trace of random samples to a value. We show that the distribution induced by integration over the space of traces equals the distribution-based semantics. Our second contribution is to formalize the implementation technique of trace
Markov chain Monte Carlo
(MCMC) for our calculus and to show its correctness. A key step is defining sufficient conditions for the distribution induced by trace MCMC to converge to the distribution-based semantics. To the best of our knowledge, this is the first rigorous correctness proof for trace MCMC for a higher-order functional language, or for a language with soft constraints.