| 1. |
- Andersen, Jörgen H., et al.
(författare)
-
A Machine Verified Distributed Sorting Algorithm
- 1996
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We present a verification of a distributed sorting algorithm in ALF, an implementation of Martin Löf's type theory. The implementation is expressed as a program in a priortized version of CBS, (the Calculus of Broadcasting Systems) which we have implemented in ALF. The specification is expressed in terms of an ALF type which represents the set of all sorted lists and an HML (Hennesey-Milner Logic) formula which expresses that the sorting program will input any number of data until it hears a value triggering the program to begin outputting the data in a sorted fashion. We gain expressive power from the type theory by inheriting the language of data, state expressions, and propositions.
|
|
| 2. |
- Harcourt, Ed, et al.
(författare)
-
A Framework for Representing Parameterised Processes
- 1995
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We describe a faithful representation of value-passing recursive parametric CCS processes in Alf, an implementation of Martin-Lof's constructive type theory. The representation is interesting because we borrow as much as possible from Alf including the domain of value and state expressions and the ability to evaluate them. Usually substitution of either channel values for channel variables and processes for process variables play a necessary role in the semantics. However, substitution is also borrowed from Alf by using higher-order functions. The main importance of this representation is that it allows us to borrow Alf's off-the-shelf theorems about data types and provides a uniform setting for doing various kinds machine assisted proofs, such as bisimulation proofs, equational reasoning, verification of Hennessy-Milner logic formulas. 1 Introduction Machine checked proofs of CCS processes require finite representations of the processes. However, for infinite value and state domains,...
|
|
| 3. |
- Kumar, Nitin, et al.
(författare)
-
Adaptation of host transmission cycle during Clostridium difficile speciation
- 2019
-
Ingår i: Nature Genetics. - : Nature Publishing Group. - 1061-4036 .- 1546-1718. ; 51:9, s. 1315-1320
-
Tidskriftsartikel (refereegranskat)abstract
- Bacterial speciation is a fundamental evolutionary process characterized by diverging genotypic and phenotypic properties. However, the selective forces that affect genetic adaptations and how they relate to the biological changes that underpin the formation of a new bacterial species remain poorly understood. Here, we show that the spore-forming, healthcare-associated enteropathogen Clostridium difficile is actively undergoing speciation. Through large-scale genomic analysis of 906 strains, we demonstrate that the ongoing speciation process is linked to positive selection on core genes in the newly forming species that are involved in sporulation and the metabolism of simple dietary sugars. Functional validation shows that the new C. difficile produces spores that are more resistant and have increased sporulation and host colonization capacity when glucose or fructose is available for metabolism. Thus, we report the formation of an emerging C. difficile species, selected for metabolizing simple dietary sugars and producing high levels of resistant spores, that is adapted for healthcare-mediated transmission.
|
|
