102 research outputs found

    Leibniz equality is isomorphic to Martin-Löf identity, parametrically

    No full text
    sponsorship: We are indebted to the reviewers of our manuscript, whose feedback helped us to great improvements. Andreas Abel acknowledges support by the Swedish Research Council through grant 621-2014-4864 Termination Certificates for Dependently-Typed Programs and Proofs via Refinement Types and by the EU Cost Action CA15123 Types for programming and verification. Philip Wadler acknowledges support from UK EPSRC programme grant EP/K034413/1 ABCD: A Basis for Concurrency and Distribution. Dominique Devriese held a Postdoctoral Fellowship of the Research Fund -Flanders (FWO) during part of the development of this work. (Swedish Research Council|621-2014-4864, EU Cost Action Types for programming and verification|CA15123, UK EPSRC programme|EP/K034413/1, Research Fund -Flanders (FWO), EPSRC|EP/K034413/1, Engineering and Physical Sciences Research Council|EP/K034413/1)status: Publishe

    Reasoning about a machine with local capabilities: Provably safe stack and return pointer management

    No full text
    © The Author(s) 2018. Capability machines provide security guarantees at machine level which makes them an interesting target for secure compilation schemes that provably enforce properties such as control-flow correctness and encapsulation of local state. We provide a formalization of a representative capability machine with local capabilities and study a novel calling convention. We provide a logical relation that semantically captures the guarantees provided by the hardware (a form of capability safety) and use it to prove control-flow correctness and encapsulation of local state. The logical relation is not specific to our calling convention and can be used to reason about arbitrary programs.sponsorship: (This research was supported in part by the ModuRes Sapere Aude Advanced Grant from The Danish Council for Independent Research for the Natural Sciences (FNU). Dominique Devriese holds a Postdoctoral fellowship from the Research Foundation Flanders (FWO).)status: Publishe

    Skeletal muscle mass in head and neck cancer patients: Radiological assessment and association with clinical outcome

    No full text
    In recent years, it has been shown that routinely performed imaging, such as computed tomography (CT) scans, can be used to extract additional information on patient’s functional and biological status, which may be used to identify patients at increased risk of adverse outcomes during and after treatment. Low skeletal muscle mass is the most known example of this application; research has shown that modern imaging such as CT or MRI can be used to accurately assess skeletal muscle quantity. Our research shows that the quantity of skeletal muscle mass can easily and reliably be assessed on CT imaging of the head and neck area. Low skeletal muscle mass, as identified on routinely performed CT and MRI of the head and neck area, is associated with increased chemotherapy dose-limiting toxicity, increased pharyngocutaneous fistula formation after total laryngectomy and decreased overall survival in several head and neck patient categories. These results are in concurrence with results in other types of cancer. Routinely performed imaging can also be used to assess the presence of arterial calcification, as a proxy for cardiovascular disease. Concluding, routinely performed imaging does not only provide easily accessible and clinically relevant information on disease status, but also holds valuable information on body composition of a patient, which may be used in individualized risk stratification, treatment adaptation and patient optimization strategies to ultimately decrease short-term adverse outcomes and increase survival

    Sarcopenia in head and neck cancer: Towards personalized medicine

    No full text
    This thesis showed that low skeletal muscle mass (sarcopenia) is a prevalent problem which occurs in approximately 55% of patients. Skeletal muscle mass can be easily assessed on a single slice at the level of C3 (or L3) on routinely performed CT or MRI scans which are performed for head and neck cancer diagnosis and treatment evaluation. Skeletal muscle mass is a promising imaging biomarker which predicts negative treatment outcomes in various treatment strategies applied in head and neck cancer management. Besides negative treatment outcomes, low skeletal muscle mass has also shown to be prognostic for decreased survival. We hypothesize that multimodal pre-habilitation will improve skeletal muscle mass status of the patient before treatment which will lead to an enhanced recovery trajectory with reduced operative complications and postoperative adverse effects in surgically treated patients and to reduced treatment-related toxicities in patients treated with (chemo- or bio) radiotherapy. We also hypothesize that multimodal pre-habilitation leads to a reduced duration of hospital stay, reduced health care costs and improved quality of life. In addition, pre-habilitation is an opportunity to foster patient empowerment which increases patient’s autonomy and self-management. This may facilitate an improved quality of life before treatment and may positively affect long-term health. Therefore, the aims of a future randomized controlled trial should be to compare the effect of a multimodal pre-habilitation program including exercise, nutritional support and psychological support with usual care on treatment outcomes and prognosis for patients with head and neck cancer, particularly those with low skeletal muscle mass. Further research is needed to validate these hypotheses. This thesis provides information that can contribute to the development of these studies

    Coagulase-negative staphylococci in bovine sub-clinical mastitis

    No full text
    Mastitis is a common disease in dairy cows. The majority of the cases are sub-clinical, and many of those are due to infection with coagulase-negative staphylococci (CNS). CNS is a heterogeneous group of bacteria consisting of a large number of different species, but limited information is available on the epidemiology of mastitis due to these species. The overall aim of the thesis was to improve the knowledge on prevalence and significance of different CNS species in connection with sub-clinical mastitis in dairy cows. In the first study, the epidemiology of CNS species, i.e. ability to induce persistent intra-mammary infections (IMI), and association with milk production, SCC, parity and month of lactation, was studied in dairy herds with problems due to sub-clinical CNS mastitis. The most commonly isolated CNS species were S. epidermidis, S. simulans, S. chomogenes, S. xylosus and S. haemolyticus. Persistent IMI were common in quarters infected with S. chromogenes, S. epidermidis and S. simulans. The results did not indicate differences between these CNS species in their association with daily milk production, cow SCC, and month of lactation. S. epidermidis was mainly found in multiparous cows, and S. chromogenes in primiparous cows. The second study concentrated on S. epidermidis by investigating possible transmission of S. epidermidis from milkers to cows, the discriminatory capacity of the sub-typing methods used and the clonal diversity within unrelated bovine S. epidermidis strains. Pulsed-field gel electrophoresis had high discriminatory power and showed that many different S. epidermidis types exist in bovine milk samples. Identical isolates were found in samples from the milker's skin and in milk samples. As dairy cows are not a natural host for S. epidermidis the results suggest a human source of these udder infections

    Finally tagless observable recursion for an grammar model

    No full text
    We define a finally tagless, shallow embedding of a typed grammar language. In order to avoid the limitations of traditional parser combinator libraries (no bottom-up parsing, no full grammar analysis or transformation), we require object-language recursion to be observable in the meta-language. Since existing proposals for recursive constructs are not fully satisfactory, we propose new finally tagless primitive recursive constructs to solve the problem. To do this in a well-typed way, we require considerable infrastructure, for which we reuse techniques from the multirec generic programming library. Our infrastructure allows a precise model of the complex interaction between a grammar, a parsing algorithm and a set of semantic actions. On the flip side, our approach requires the grammar author to provide a type-and value-level encoding of the grammar's domain and we can provide only a limited form of constructs like many. We demonstrate five meta-language grammar algorithms exploiting our model, including a grammar pretty-printer, a reachability analysis, a translation of quantified recursive constructs to the standard one and an implementation of the left-corner grammar transform. The work we present forms the basis of the grammar-combinators parsing library 1, which is the first to work with a precise, shallow model of context-free grammars in a classical (not dependently typed) functional language and which supports a wide range of grammar manipulation primitives. From a more general point of view, our work shows a solution to the well-studied problem of observable sharing in shallowly embedded domain-specific languages and specifically in finally tagless domain-specific languages. ©2012 Copyright Cambridge University Press.sponsorship: This research is partially funded by the Interuniversity Attraction Poles Programme Belgian State (Belgian Science Policy), the Research Foundation - Flanders (FWO) and the Research Fund K.U. Leuven. Dominique Devriese holds a PhD fellowship of the Research Foundation - Flanders (FWO). We thank Arie Middelkoop, Tom Schrijvers, Adriaan Moors, Doaitse Swierstra, Nils Anders Danielsson and anonymous reviewers for their comments. (Interuniversity Attraction Poles Programme Belgian State (Belgian Science Policy), Research Foundation - Flanders (FWO), Research Fund K.U. Leuven)status: Publishe
    corecore