| 1. |
- Adams, Robin, 1978
(författare)
-
A Modular Hierarchy of Logical Frameworks
- 2004
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. ; 3085, s. 1-16
-
Konferensbidrag (refereegranskat)abstract
- We present a method for defining logical frameworks as a collection of features which are defined and behave independently of one another. Each feature is a set of grammar clauses and rules of deduction such that the result of adding the feature to a framework is a conservative extension of the framework itself. We show how several existing logical frameworks can be so built, and how several much weaker frameworks defined in this manner are adequate for expressing a wide variety of object logics.
|
|
| 2. |
- Adams, Robin, 1978, et al.
(författare)
-
A pluralist approach to the formalisation of mathematics
- 2011
-
Ingår i: Mathematical Structures in Computer Science. - 0960-1295 .- 1469-8072. ; 21:4, s. 913-942
-
Tidskriftsartikel (refereegranskat)abstract
- We present a programme of research for pluralist formalisations, that is, formalisations that involve proving results in more than one foundation.A foundation consists of two parts: a logical part, which provides a notion of inference, and a non-logical part, which provides the entities to be reasoned about. An LTT is a formal system composed of two such separate parts. We show how LTTs may be used as the basis for a pluralist formalisation.We show how different foundations may be formalised as LTTs, and also describe a new method for proof reuse. If we know that a translation Φ exists between two logic-enriched type theories (LTTs) S and T, and we have formalised a proof of a theorem α in S, we may wish to make use of the fact that Φ(α) is a theorem of T. We show how this is sometimes possible by writing a proof script MΦ. For any proof script Mα that proves a theorem α in S, if we change Mα so it first imports MΦ, the resulting proof script will still parse, and will be a proof of Φ(α) in T.In this paper, we focus on the logical part of an LTT-framework and show how the above method of proof reuse is done for four cases of Φ: inclusion, the double negation translation, the A-translation and the Russell–Prawitz modality. This work has been carried out using the proof assistant Plastic.
|
|
| 3. |
- Adams, Robin, 1978, et al.
(författare)
-
A Type Theory for Probabilistic and Bayesian Reasoning
- 2018
-
Ingår i: Leibniz International Proceedings in Informatics (LIPIcs). - 1868-8969. - 9783959770309 ; 69, s. 11-134
-
Konferensbidrag (refereegranskat)abstract
- This paper introduces a novel type theory and logic for probabilistic reasoning. Its logic is quantitative, with fuzzy predicates. It includes normalisation and conditioning of states. This conditioning uses a key aspect that distinguishes our probabilistic type theory from quantum type theory, namely the bijective correspondence between predicates and side-effect free actions (called instrument, or assert, maps). The paper shows how suitable computation rules can be derived from this predicate-action correspondence, and uses these rules for calculating conditional probabilities in two well-known examples of Bayesian reasoning in (graphical) models. Our type theory may thus form the basis for a mechanisation of Bayesian inference.
|
|
| 4. |
- Adams, Robin, 1978, et al.
(författare)
-
Classical Predicative Logic-Enriched Type Theories
- 2010
-
Ingår i: Annals of Pure and Applied Logic. - : Elsevier BV. - 0168-0072. ; 161:11, s. 1315-1345
-
Tidskriftsartikel (refereegranskat)abstract
- A logic-enriched type theory (LTT) is a type theory extended with a primitive mechanism for forming and proving propositions. We construct two LTTs, named LTT0 and LTT0*, which we claim correspond closely to the classical predicative systems of second order arithmetic ACA0 and ACA0*. We justify this claim by translating each second order system into the corresponding LTT, and proving that these translations are conservative. This is part of an ongoing research project to investigate how LTTs may be used to formalise different approaches to the foundations of mathematics. The two LTTs we construct are subsystems of the logic-enriched type theory LTTW, which is intended to formalise the classical predicative foundation presented by Herman Weyl in his monograph Das Kontinuum. The system has also been claimed to correspond to Weyl’s foundation. By casting ACA0 and ACA as LTTs, we are able to compare them with LTTW. It is a consequence of the work in this paper that LTTW is strictly stronger than ACA0. The conservativity proof makes use of a novel technique for proving one LTT conservative over another, involving defining an interpretation of the stronger system out of the expressions of the weaker. This technique should be applicable in a wide variety of different cases outside the present work.
|
|
| 5. |
- Adams, Robin, 1978
(författare)
-
Coercive subtyping in lambda-free logical frameworks
- 2009
-
Konferensbidrag (refereegranskat)abstract
- We show how coercive subtyping may be added to a lambda-free logical framework, by constructing the logical framework TF<, an extension of the lambda-free logical framework TF with coercive subtyping. Instead of coercive application, TF< makes use of a typecasting operation. We develop the metatheory of the resulting framework, including providing some general conditions under which typecasting in an object theory with coercive subtyping is decidable. We show how TF< may be embedded in the logical framework LF, and hence how results about LF may be deduced from results about TF< .
|
|
| 6. |
- Adams, Robin, 1978, et al.
(författare)
-
Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing between Black-Box Components
- 2018
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 11294, s. 196-214
-
Konferensbidrag (refereegranskat)abstract
- Privacy by design (PbD) is the principle that privacy should be considered at every stage of the software engineering process. It is increasingly both viewed as best practice and required by law. It is therefore desirable to have formal methods that provide guarantees that certain privacy-relevant properties hold. We propose an approach that can be used to design a privacy-compliant architecture without needing to know the source code or internal structure of any individual component. We model an architecture as a set of agents or components that pass messages to each other. We present in this paper algorithms that take as input an architecture and a set of privacy constraints, and output an extension of the original architecture that satisfies the privacy constraints.
|
|
| 7. |
- Adams, Robin, 1978
(författare)
-
Formalized metatheory with terms represented by an indexed family of types
- 2006
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. ; 3839, s. 1-16
-
Konferensbidrag (refereegranskat)abstract
- It is possible to represent the terms of a syntax with binding constructors by a family of types, indexed by the free variables that may occur. This approach has been used several times for the study of syntax and substitution, but never for the formalization of the metatheory of a typing system. We describe a recent formalization of the metatheory of Pure Type Systems in Coq as an example of such a formalization. In general, careful thought is required as to how each definition and theorem should be stated, usually in an unfamiliar ‘big-step’ form; but, once the correct form has been found, the proofs are very elegant and direct.
|
|
| 8. |
|
|
| 9. |
- Adams, Robin, 1978
(författare)
-
Pure type systems with judgemental equality
- 2006
-
Ingår i: Journal of Functional Programming. - 1469-7653 .- 0956-7968. ; 16:2, s. 219-246
-
Tidskriftsartikel (refereegranskat)abstract
- In a typing system, there are two approaches that may be taken to the notion of equality. One can use some external relation of convertibility defined on the terms of the grammar, such as $\beta$-convertibility or $\beta \eta$-convertibility; or one can introduce a judgement form for equality into the rules of the typing system itself. For quite some time, it has been an open problem whether the two systems produced by these two choices are equivalent. This problem is essentially the problem of proving that the Subject Reduction property holds in the system with judgemental equality. In this paper, we shall prove that the equivalence holds for all functional Pure Type Systems (PTSs). The proof essentially consists of proving the Church-Rosser Theorem for a typed version of parallel one-step reduction. This method should generalise easily to many typing systems which satisfy the Uniqueness of Types property.
|
|
| 10. |
- Adams, Robin, 1978
(författare)
-
QPEL: Quantum Program and Effect Language
- 2014
-
Ingår i: Electronic Proceedings in Theoretical Computer Science. - 2075-2180. ; 172, s. 133-153
-
Konferensbidrag (refereegranskat)abstract
- We present the syntax and rules of deduction of QPEL (Quantum Program and Effect Language), a language for describing both quantum programs, and properties of quantum programs - effects on the appropriate Hilbert space. We show how semantics may be given in terms of state-and-effect triangles, a categorical setting that allows semantics in terms of Hilbert spaces, C*-algebras, and other categories. We prove soundness and completeness results that show the derivable judgements are exactly those provable in all state-and-effect triangles.
|
|
