| 1. |
- Abrahamsson, Oskar, 1986, et al.
(author)
-
Proof-Producing Synthesis of CakeML from Monadic HOL Functions
- 2020
-
In: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 64:7, s. 1287-1306
-
Journal article (peer-reviewed)abstract
- We introduce an automatic method for producing stateful ML programs together with proofs of correctness from monadic functions in HOL. Our mechanism supports references, exceptions, and I/O operations, and can generate functions manipulating local state, which can then be encapsulated for use in a pure context. We apply this approach to several non-trivial examples, including the instruction encoder and register allocator of the otherwise pure CakeML compiler, which now benefits from better runtime performance. This development has been carried out in the HOL4 theorem prover.
|
|
| 2. |
- Ahrens, B., et al.
(author)
-
From Signatures to Monads in UniMath
- 2019
-
In: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 63:2, s. 285-318
-
Journal article (peer-reviewed)abstract
- The term UniMath refers both to a formal system for mathematics, as well as a computer-checked library of mathematics formalized in that system. The UniMath system is a core dependent type theory, augmented by the univalence axiom. The system is kept as small as possible in order to ease verification of it-in particular, general inductive types are not part of the system. In this work, we partially remedy the lack of inductive types by constructing some set-level datatypes and their associated induction principles from other type constructors. This involves a formalization of a category-theoretic result on the construction of initial algebras, as well as a mechanism to conveniently use the datatypes obtained. We also connect this construction to a previous formalization of substitution for languages with variable binding. Altogether, we construct a framework that allows us to concisely specify, via a simple notion of binding signature, a language with variable binding. From such a specification we obtain the datatype of terms of that language, equipped with a certified monadic substitution operation and a suitable recursion scheme. Using this we formalize the untyped lambda calculus and the raw syntax of Martin-Lof type theory.
|
|
| 3. |
|
|
| 4. |
- Bengtson, Jesper, et al.
(author)
-
Psi-Calculi in Isabelle
- 2016
-
In: Journal of automated reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 56:1, s. 1-47
-
Journal article (peer-reviewed)abstract
- This paper presents a mechanisation of psi-calculi, a parametric framework for modelling various dialects of process calculi including (but not limited to) the pi-calculus, the applied pi-calculus, and the spi calculus. psi-calculi are significantly more expressive, yet their semantics is as simple in structure as the semantics of the original pi-calculus. Proofs of meta-theoretic properties for psi-calculi are more involved, however, not least because psi-calculi (unlike simpler calculi) utilise binders that bind multiple names at once. The mechanisation is carried out in the Nominal Isabelle framework, an interactive proof assistant designed to facilitate formal reasoning about calculi with binders. Our main contributions are twofold. First, we have developed techniques that allow efficient reasoning about calculi that bind multiple names in Nominal Isabelle. Second, we have adopted these techniques to mechanise substantial results from the meta-theory of psi-calculi, including congruence properties of bisimilarity and the laws of structural congruence. To our knowledge, this is the most extensive formalisation of process calculi mechanised in a proof assistant to date.
|
|
| 5. |
- Bezem, M., et al.
(author)
-
The Univalence Axiom in Cubical Sets
- 2019
-
In: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 63:2, s. 159-171
-
Journal article (peer-reviewed)abstract
- In this note we show that Voevodsky's univalence axiom holds in the model of type theory based on cubical sets as described inBezem et al. (in: Matthes and Schubert (eds.) 19th international conference on types for proofs and programs (TYPES 2013), Leibniz international proceedings in informatics (LIPIcs), Schloss Dagstuhl-Leibniz-Zentrum fur Informatik, Dagstuhl, Germany, vol26, pp 107-128, 2014. 10.4230/LIPIcs.TYPES.2013.107. http://drops.dagstuhl.de/opus/volltexte/2014/4628) and Huber (A model of type theory in cubical sets. Licentiate thesis, University of Gothenburg, 2015). We will also discuss Swan's construction of the identity type in this variation of cubical sets. This proves that we have a model of type theory supporting dependent products, dependent sums, univalent universes, and identity types with the usual judgmental equality, and this model is formulated in a constructive metatheory.
|
|
| 6. |
- Birkedal, Lars, et al.
(author)
-
Guarded Cubical Type Theory
- 2019
-
In: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 63:2, s. 211-253
-
Journal article (peer-reviewed)abstract
- This paper improves the treatment of equality in guarded dependent type theory ((Formula presented.)), by combining it with cubical type theory ((Formula presented.)). (Formula presented.) is an extensional type theory with guarded recursive types, which are useful for building models of program logics, and for programming and reasoning with coinductive types. We wish to implement (Formula presented.) with decidable type checking, while still supporting non-trivial equality proofs that reason about the extensions of guarded recursive constructions. (Formula presented.) is a variation of Martin–Löf type theory in which the identity type is replaced by abstract paths between terms. (Formula presented.) provides a computational interpretation of functional extensionality, enjoys canonicity for the natural numbers type, and is conjectured to support decidable type-checking. Our new type theory, guarded cubical type theory ((Formula presented.)), provides a computational interpretation of extensionality for guarded recursive types. This further expands the foundations of (Formula presented.) as a basis for formalisation in mathematics and computer science. We present examples to demonstrate the expressivity of our type theory, all of which have been checked using a prototype type-checker implementation. We show that (Formula presented.) can be given semantics in presheaves on (Formula presented.), where (Formula presented.) is the cube category, and (Formula presented.) is any small category with an initial object. We then show that the category of presheaves on (Formula presented.) provides semantics for (Formula presented.).
|
|
| 7. |
- Björk, Magnus, 1977
(author)
-
First Order Stålmarck
- 2009
-
In: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 42:1, s. 99-122
-
Journal article (peer-reviewed)abstract
- We present a proof method with a novel way of introducing universal lemmas. The method is a first order extension of StAyenlmarck's method, containing a branch-and-merge rule known as the dilemma rule. The dilemma rule creates two branches in a tableau-like way, but later recombines the two branches, keeping the common consequences. While the propositional version uses normal set intersection in the merges, the first order version searches for pairwise unifiable formulae in the two branches. Within branches, the system uses a special kind of variables that may not be substituted. At branch merges, these variables are replaced by universal variables, and in this way universal lemmas can be introduced. Relevant splitting formulae are found through failed unifications of variables in branches. This article presents the calculus and proof procedure, and shows soundness and completeness. Benchmarks of an implementation are also presented.
|
|
| 8. |
- Bonacina, M.P., et al.
(author)
-
Interpolation Systems for Ground Proofs in Automated Deduction: a Survey
- 2015
-
In: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 54:4, s. 353-390
-
Journal article (peer-reviewed)abstract
- Interpolation is a deductive technique applied in program analysis and verification: for example, it is used to compute over-approximations of images or refine abstractions. An interpolation system takes a refutation and extracts an interpolant by building it inductively from partial interpolants. We survey color-based interpolation systems for ground proofs produced by key inference engines of state-of-the-art solvers: DPLL for propositional logic, equality sharing for combination of convex theories, and DPLL((Formula presented.)) for SMT-solving. Since color-based interpolation systems use colors to track symbols in proofs, equality is problematic, because replacement of equals by equals mixes symbols and therefore colors. We analyze interpolation in the presence of equality, and we demonstrate the color-based approach by giving a complete interpolation system for ground proofs by superposition.
|
|
| 9. |
- Bonacina, M.P., et al.
(author)
-
On Interpolation in Automated Theorem Proving
- 2015
-
In: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 54:1, s. 69-97
-
Journal article (peer-reviewed)abstract
- Given two inconsistent formul', a (reverse) interpolant is a formula implied by one, inconsistent with the other, and only containing symbols they share. Interpolation finds application in program analysis, verification, and synthesis, for example, towards invariant generation. An interpolation system takes a refutation of the inconsistent formul' and extracts an interpolant by building it inductively from partial interpolants. Known interpolation systems for ground proofs use colors to track symbols. We show by examples that the color-based approach cannot handle non-ground refutations by resolution and paramodulation/superposition. We present a two-stage approach that works by tracking literals, computes a provisional interpolant, which may contain non-shared symbols, and applies lifting to replace non-shared constants by quantified variables. We obtain an interpolation system for non-ground refutations, and we prove that it is complete, if the only non-shared symbols in provisional interpolants are constants.
|
|
| 10. |
- Brillout, Angelo, et al.
(author)
-
An interpolating sequent calculus for quantifier-free Presburger arithmetic
- 2011
-
In: Journal of automated reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 47:4, s. 341-367
-
Journal article (peer-reviewed)abstract
- Craig interpolation has become a versatile tool in formal verification, used for instance to generate program assertions that serve as candidates for loop invariants. In this paper, we consider Craig interpolation for quantifier-free Presburger arithmetic (QFPA). Until recently, quantifier elimination was the only available interpolation method for this theory, which is, however, known to be potentially costly and inflexible. We introduce an interpolation approach based on a sequent calculus for QFPA that determines interpolants by annotating the steps of an unsatisfiability proof with partial interpolants. We prove our calculus to be sound and complete. We have extended the Princess theorem prover to generate interpolating proofs, and applied it to a large number of publicly available Presburger arithmetic benchmarks. The results document the robustness and efficiency of our interpolation procedure. Finally, we compare the procedure against alternative interpolation methods, both for QFPA and linear rational arithmetic.
|
|
