354 papers · page 11 of 18
Blockchain technology has increasing attention in research and across many industries. The Ethereum blockchain offers smart contracts, which are small programs defined, executed, and recorded as transactions in the blockchain transaction history. These smart contracts run on the …
Search-based satisfiability procedures try to construct a model of the input formula by simultaneously proposing candidate models and deriving new formulae implied by the input. When the formulae are satisfiable, these procedures generate a model as a witness. Dually, it is desir…
Lambda-tree syntax (λTS), also known as higher-order abstract syntax (HOAS), is a representational technique where the pure λ-calculus in a meta-language is used to represent binding constructs in an object language. A key feature of λTS is that capture-avoiding substitution in t…
Matrix interpretations are widely used in automated complexity analysis. Certifying such analyses boils down to determining the growth rate of An for a fixed non-negative rational matrix A. A direct solution for this task involves the computation of all eigenvalues of A, which of…
Semi-algebraic sets and semi-algebraic functions are essential to specify and certify cylindrical algebraic decomposition algorithms. We formally define in Coq the base operations on semi-algebraic sets and functions using embedded first-order formulae over the language of real c…
The completeness proofs for Propositional Dynamic Logic (PDL) in the literature are non-constructive and usually presented in an informal manner. We obtain a formal and constructive completeness proof for Converse PDL by recasting a completeness proof by Kozen and Parikh into our…
We present a Coq library that allows for readily proving that a function is computable in polynomial time. It is based on quasi-interpretations that, in combination with termination ordering, provide a characterisation of the class fp of functions computable in polynomial time. A…
This paper presents generic derivations of induction for impredicatively typed lambda-encoded datatypes, in the Cedille type theory. Cedille is a pure type theory extending the Curry-style Calculus of Constructions with implicit products, primitive heterogeneous equality, and dep…
Based on our earlier formalization of conflict-driven clause learning (CDCL) in Isabelle/HOL, we refine the CDCL calculus to add a crucial optimization: two watched literals. We formalize the data structure and the invariants. Then we refine the calculus to obtain an executable S…
We study different formalizations of finite sets in homotopy type theory to obtain a general definition that exhibits both the computational facilities and the proof principles expected from finite sets. We use higher inductive types to define the type K(A) of "finite sets over t…
Relational properties describe multiple runs of one or more programs. They characterize many useful notions of security, program refinement, and equivalence for programs with diverse computational effects, and they have received much attention in the recent literature. Rather tha…
The de Bruijn representation of syntax with binding is commonly used, but flawed when it comes to recursion. As the structural recursion principle associated to an inductive type of expressions is unaware of the binding discipline, each recursive definition requires a separate pr…
Economic activity has always been a fundamental part of society. With recent social and political changes economics has gained even more influence on our lives. In this paper we formalize two economic models in Isabelle/HOL: the pure exchange economy, where the only economic acto…
We study various models of classical second-order set theories in the dependent type theory of Coq. Without logical assumptions, Aczel’s sets-as-trees interpretation yields an intensional model of second-order ZF with functional replacement. Building on work of Werner and Barras,…
We propose a formalization of HOπ in Coq, a process calculus where messages carry processes. Such a higher-order calculus features two very different kinds of binder: process input, similar to λ-abstraction, and name restriction, whose scope can be expanded by communication. We f…
The idea of a context lemma spans a range of programming-language models: from Milner’s original through the CIU theorem to ‘CIU-like’ results for multiple language features. Each shows that to prove observational equivalence between program terms it is enough to test only some r…
Verifying systems by implementing them in the programming language of a proof assistant (e.g., Gallina for Coq) lets us directly leverage the full power of the proof assistant for verifying the system. But, to execute such an implementation requires extraction, a large complicate…
Mechanizing formal systems, given via axioms and inference rules, together with proofs about them plays an important role in establishing trust in formal developments. Over the past decade, the POPLMark challenge popularized the use of proof assistants in mechanizing the metatheo…
We present the first formalisation of a blockchain-based distributed consensus protocol with a proof of its consistency mechanised in an interactive proof assistant.
We extend proof automation in an interactive theorem prover to analyze changes in specifications and proofs. Our approach leverages the history of changes to specifications and proofs to search for a patch that can be applied to other specifications and proofs that need to change…