| 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 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.
|
|
| 3. |
- 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< .
|
|
| 4. |
- 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.
|
|
| 5. |
- 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.
|
|
| 6. |
- 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.
|
|
| 7. |
- Adams, Robin, 1978, et al.
(författare)
-
Weyl's predicative classical mathematics as a logic-enriched type theory
- 2007
-
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. ; 4502, s. 1-17
-
Konferensbidrag (refereegranskat)abstract
- In Das Kontinuum, Weyl showed how a large body of classical mathematics could be developed on a purely predicative foundation. We present a logic-enriched type theory that corresponds to Weyl’s foundational system. A large part of the mathematics in Weyl’s book — including Weyl’s definition of the cardinality of a set and several results from real analysis — has been formalised, using the proof assistant Plastic that implements a logical framework. This case study shows how type theory can be used to represent a non-constructive foundation for mathematics.
|
|
| 8. |
- Bezem, Marc, et al.
(författare)
-
A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic
- 2018
-
Ingår i: Leibniz International Proceedings in Informatics, LIPIcs. - 1868-8969. ; 97
-
Konferensbidrag (refereegranskat)abstract
- The univalence axiom expresses the principle of extensionality for dependent type theory. However, if we simply add the univalence axiom to type theory, then we lose the property of canonicity— that every closed term computes to a canonical form. A computation becomes ‘stuck’ when it reaches the point that it needs to evaluate a proof term that is an application of the univalence axiom. So we wish to find a way to compute with the univalence axiom. While this problem has been solved with the formulation of cubical type theory, where the computations are expressed using a nominal extension of lambda-calculus, it may be interesting to explore alternative solutions, which do not require such an extension.As a first step, we present here a system of propositional higher-order minimal logic (PHOML). There are three kinds of typing judgement in PHOML. There are terms which inhabit types, which are the simple types over Ω. There are proofs which inhabit propositions, which are the terms of type Ω. The canonical propositions are those constructed from ⊥ by implication ⊃. Thirdly, there are paths which inhabit equations M = A N , where M and N are terms of type A. There are two ways to prove an equality: reflexivity, and propositional extensionality — logically equivalent propositions are equal. This system allows for some definitional equalities that are not present in cubical type theory, namely that transport along the trivial path is identity. We present a call-by-name reduction relation for this system, and prove that the system satisfies canonicity: every closed typable term head-reduces to a canonical form. This work has been formalised in Agda.
|
|
| 9. |
- Buvendiek, Kai, et al.
(författare)
-
Privacy-Preserving Architectures with Probabilistic Guaranties
- 2018
-
Ingår i: 2018 16th Annual Conference on Privacy, Security and Trust, PST 2018. - 9781538674932 ; , s. 38-47
-
Konferensbidrag (refereegranskat)abstract
- Violations of the privacy of users can happen if data protection is not a fundamental part of the development process of a software system. The principle of Privacy by Design (PbD) therefore stipulates the consideration of privacy as a default feature. We have developed an integrated tool environment called CAPVerDE that provides a formal description language of software architectures and helps a designer by automatically verifying data minimization properties the architectural level. Our logic includes probabilistic properties that introduce uncertainty into the architectures. These properties can be used to model attack scenarios that rely on chance. This paper presents the logic of the description language of CAPVerDE and illustrates the reasoning by applying it to a smart energy metering case study.
|
|
| 10. |
|
|
