CertiCoq is a mechanically verified, optimizing compiler for Coq that bridges the gap between certified high-level programs and their translation to machine language. We outline its design as well as the main foundational and engineering challenges involved in building and certifying a compiler for Coq in Coq.

SAFE is a clean-slate design for a highly secure computer system, with pervasive mechanisms for tracking and limiting information flows. At the lowest level, the SAFE hardware supports fine-grained programmable tags, with efficient and flexible propagation and combination of tags as instructions are executed. The operating system virtualizes these generic facilities to present an information-flow abstract machine that allows user programs to label sensitive data with rich confidentiality policies. We present a formal, machine-checked model of the key hardware and software mechanisms used to control information flow in SAFE and an end-to-end proof of noninterference for this model.

We provide an overview of the FET-Open Project CerCo ('Certified Complexity'). Our main achievement is the development of a technique for analysing non-functional properties of programs (time, space) at the source level with little or no loss of accuracy and a small trusted code base. The core component is a C compiler, verified in Matita, that produces an instrumented copy of the source code in addition to generating object code. This instrumentation exposes, and tracks precisely, the actual (non-asymptotic) computational cost of the input program at the source level. Untrusted invariant generators and trusted theorem provers may then be used to compute and certify the parametric execution time of the code.

The security literature offers a multitude of calculi, languages, and systems for information-flow control, each with some set of labels encoding security policies that can be attached to data and computations. The exact form of these labels varies widely, with different systems offering many different combinations of features addressing issues such as confidentiality, integrity, and policy ownership. This variation makes it difficult to compare the expressive power of different information-flow frameworks. To enable such comparisons, we introduce label algebras, an abstract interface for information-flow labels equipped with a notion of authority, and study several notions of embedding between them. The simplest is a straightforward notion of injection between label algebras, but this lacks a clear computational motivation and rejects some reasonable encodings between label models. We obtain a more refined account by defining a space of encodings parameterized by an interpretation of labels and authorities, thus giving a semantic flavor to the definition of encoding. We study the theory of semantic encodings and consider two specific instances, one based on the possible observations of boolean values and one based on the behavior of programs in a small lambda-calculus parameterized over an arbitrary label algebra. We use this framework to define and compare a number of concrete label algebras, including realizations of the familiar taint, endorsement, readers, and distrust models, as well as label algebras based on several existing programming languages and operating systems.

In this paper we introduce the notion of map, which is a notation for the set of occurrences of a symbol in a syntactic expression such as a formula or a lambda term. We use binary trees over 0 and 1 as maps, but some well-formedness conditions are required. We develop a representation of lambda terms using maps. The representation is concrete (inductively definable in HOL or Constructive Type Theory) and canonical (one representative per lambda term). We define substitution for our map representation, and prove the representation is in substitution preserving isomorphism with both nominal logic lambda terms and de Bruijn nameless terms. These proofs are mechanically checked in Isabelle/HOL and Minlog respectively.The map representation has good properties. Substitution does not require adjustment of binding information: neither alpha conversion of the body being substituted into, nor de Bruijn lifting of the term being implanted. We have a natural proof of the substitution lemma of lambda calculus that requires no fresh names, or index manipulation.Using the notion of map we study conventional raw lambda syntax. E.g. we give, and prove correct, a decision procedure for alpha equivalence of raw lambda terms that does not require fresh names.We conclude with a definition of beta reduction for map terms, some discussion on the limitations of our current work, and suggestions for future work. (C) 2013 Royal Dutch Mathematical Society (KWG). Published by Elsevier B.V. All rights reserved.

This paper is about completely formal representation of languages with binding. We have previously written about a representation following an approach going back to Frege, based on first-order syntax using distinct syntactic classes for locally bound variables vs. global or free variables (Sato and Pollack, J Symb Comput 45:598---616, 2010). The present paper differs from our previous work by being more abstract. Whereas we previously gave a particular concrete function for canonically choosing the names of binders, here we characterize abstractly the properties required of such a choice function to guarantee canonical representation, and focus on the metatheory of the representation, proving that it is in substitution preserving isomorphism with the nominal Isabelle representation of pure lambda terms. This metatheory is formalized in Isabelle/HOL. The final section outlines a formalization in Matita of a challenging language with multiple binding and simultaneous substitution. The Isabelle and Matita proof files are available online.

Safe is a clean-slate design for a secure host architecture. It integrates advances in programming languages, operating systems, and hardware and incorporates formal methods at every step. Though the project is still at an early stage, we have assembled a set of basic architectural choices that we believe will yield a high-assurance system. We sketch the current state of the design and discuss several of these choices.

It is well known that formally defining and reasoning about languages with binding (such as logics and λ-calculii) is problematic. There are many approaches to deal with the problem, with much work over recent years stimulated by the desire to formally reason about programming languages and program logics. The various approaches have their own strengths and drawbacks, but no fully satisfactory approach has appeared. We present an approach based on two levels of syntax: an internal syntax which is convenient for machine manipulation, and an external syntax which is the usual informal syntax used in many articles and textbooks. Throughout the paper we use pure λ-calculus as an example, but the technique extends to many languages with binding. Our internal syntax is canonical: one representative of every αequivalence class. It is formalized in Isabelle/HOL, and its properties are mechanically proved. It is also proved to be isomorphic with a nominal representation of λ-calculus in Isabelle/HOL. Our conventional, human friendly external syntax is naturally related to the internal syntax by a semantic function. We do not define notions directly on the external syntax, since that would require the usual care about α-renaming, but introduce them indirectly from the canonical internal syntax via the semantic function. © 2010 Elsevier Ltd. All rights reserved.

It is well known that formally defining and reasoning about languages with binding (such as logics and lambda-calculii) is problematic. There are many approaches to deal with the problem, with much work over recent years stimulated by the desire to formally reason about programming languages and program logics. The various approaches have their own strengths and drawbacks, but no fully satisfactory approach has appeared.We present an approach based on two levels of syntax: an internal syntax which is convenient for machine manipulation, and an external syntax which is the usual informal syntax used in many articles and textbooks. Throughout the paper we use pure lambda-calculus as an example, but the technique extends to many languages with binding.Our internal syntax is canonical: one representative of every alpha-equivalence class. It is formalized in Isabelle/HOL, and its properties are mechanically proved. It is also proved to be isomorphic with a nominal representation of lambda-calculus in Isabelle/HOL.Our conventional, human friendly external syntax is naturally related to the internal syntax by a semantic function. We do not define notions directly on the external syntax, since that would require the usual care about alpha-renaming, but introduce them indirectly from the canonical internal syntax via the semantic function. (C) 2010 Elsevier Ltd. All rights reserved.

This abstract is organized as follows. In section 1 we introduce the set S[X] of symbolic expressions freely generated from a countable set X of atoms (global variables) and natural numbers (serving as a second species of names for local vari- ables). In contrast with de Bruijn indices [2] our natural number local variables are used as names, directly referring to corresponding name-carrying binders. We also introduce a new notion of B-algebra and characterize the set of symbolic ex- pressions as a free B-algebra. We define substitutions as B-algebra endomorphisms on S. Atom permutations (i.e. bijective substitutions) are automorphisms and the group of permutations acts on S, inducing a notion of equivariance. Concretely, the notion of substitution satisfies purely structural equations; there is no need for renaming variables while computing substitutions. This section closes by defining a function on S for canonically choosing the names of bound local variables. In Section 2, we introduce the internal syntax for -calculus, so called because it can be easily implemented on a computer. Rather than quotienting the raw symbolic expressions by -equivalence, as is usual, we define the set L of -terms as a subset of the free B-algebra S. Substitution (as defined on S) is closed on L. In this paper, we use the untyped -calculus as a canonical example of linguistic structure with variable binding. ? This work is an extensively revised version of [10]. 2009 Published by Elsevier Science B. V. Sato, Pollack Elsewhere, we also introduce external syntax which is intended to be used by

Machine-checked proofs of properties of programming languages have become acritical need, both for increased confidence in large and complex designsand as a foundation for technologies such as proof-carrying code. However, constructing these proofs remains a black art, involving many choices in the formulation of definitions and theorems that make a huge cumulative difference in the difficulty of carrying out large formal developments. There presentation and manipulation of terms with variable binding is a key issue. We propose a novel style for formalizing metatheory, combining locally nameless representation of terms and cofinite quantification of free variable names in inductivedefinitions of relations on terms (typing, reduction, ...). The key technical insight is that our use of cofinite quantification obviates the need for reasoning about equivariance (the fact that free names can be renamed in derivations); in particular, the structural induction principles of relations defined using cofinite quantification are strong enough for metatheoretic reasoning, and need not be explicitly strengthened. Strong inversion principles follow (automatically, in Coq) from the induction principles. Although many of the underlying ingredients of our technique have been used before, their combination here yields a significant improvement over other methodologies using first-order representations, leading to developments that are faithful to informal practice, yet require noexternal tool support and little infrastructure within the proof assistant. We have carried out several large developments in this style using the Coq proof assistant and have made them publicly available. Our developments include type soundness for System F sub; and core ML (with references, exceptions, datatypes, recursion, and patterns) and subject reduction for the Calculus of Constructions. Not only do these developments demonstrate the comprehensiveness of our approach; they have also been optimized for clarity and robustness, making them good templates for future extension.

We have presented efficient syntax directed presentations of two subclasses of PTS: The only remaining defect in these presentations lies in the possible failure of tests for conversion in the application rule. Thus for normalizing functional and semi-full systems, everything has been said. For non-functional systems the situation is less clear. We know of no a priori bound on the amount of reduction necessary to correctly type λ-abstractions, so we must be content with the collective completeness of the family of syntax directed systems ⊢sd−n. We have made little impact on the Expansion Postponement problem, which we leave as future work. We can however bask in the relative peace of mind gained from the machine-checked presentation of most (i.e. those not concerning schematic judgments) of the above results.

Our long term goal is a system to formally represent complex structured mathematical objects, and proofs and computation on such objects; e.g. a foundational computer algebra system. Our approach is informed by the long development of module systems for functional programming based on dependent record types as signatures [22]. For our logical purposes, however, we want a dependently typed base language. In this paper we propose an extension of Martin-Lof’s logical framework [25, 21] with dependently typed records, and present the semantic foundation and the typechecking algorithm of our system. Some of the work is formally checked in Coq [8].1 We have also implemented and experimented with several related systems. Our proposal combines a semantic foundation, provably sound typechecking, good expressiveness (e.g. subtyping, sharing) and first-class higher-order modules. The development of functional programming modules has addressed many aspects of the problem, such as use of manifest or transparent fields to control the information available in a signature, signature strengthening, type abstraction, sharing and subtyping [19, 15, 20]. The problem of modularity is not, however, closed, with much current research into first-class higher-order modules, recursive modules and mixins. There has also been work on dependently typed records over dependent base languages. A first practical implementation is described in [3], however without semantic foundation. An original extension of Martin-Lof’s logical framework is given in [6], however it lacks manifest fields to express sharing, and lacks metamathematical analysis. A general approach to adding modules on top of a Pure Type System

We describe a framework of algebraic structures in the proof assistant Coq. We have developed this framework as part of the FTA project in Nijmegen, in which a constructive proof of the fundamental theorem of algebra has been formalized in Coq. The algebraic hierarchy that is described here is both abstract and structured. Structures like groups and rings are part of it in an abstract way, defining e.g. a ring as a tuple consisting of a group, a binary operation and a constant that together satisfy the properties of a ring. In this way, a ring automatically inherits the group properties of the additive subgroup. The algebraic hierarchy is formalized in Coq by applying a combination of labelled record types and coercions. In the labelled record types of Coq, one can use dependent types: the type of one label may depend on another label. This allows us to give a type to a dependent-typed tuple like 〈A, f, a〉, where A is a set,f an operation on A and a an element of A. Coercions are functions that are used implicitly (they are inferred by the type checker) and allow, for example, to use the structure A: = 〈A, f, a〉 as a synonym for the carrier set A, as is often done in mathematical practice. Apart from the inheritance and reuse of properties, the algebraic hierarchy has proven very useful for reusing notations.

Abstract: SyntaxFor expressions, we have fours categories: expressions, sorts, contexts and definitional context.The abstract syntax ise; a = e e j x j s j [x = e]e j [x : a]e j fx : age j e:x j !\Gamma? j (\Delta)s = \Gamma = () j [x : a]\Gamma j [x = e]\Gamma\Delta = () j [x = e]\DeltaAs usual, we can define a 1 ! a 2 as f : a 1 ga 2 where is a special dummy name.2.2 ComputationsAn environment ae is a map ae : Dom(ae) ! (val; val) where Dom(ae) ` name. The mainoperation takes an...

We describe a framework for algebraic expressions for the proof assistant Coq. This framework has been developed as part of the FTA project in Nijmegen, in which a complete proof of the fundamental theorem of algebra has been formalized in Coq. The algebraic framework that is described here is both abstract and structured. We apply a combination of record types, coercive subtyping and implicit arguments. The algebraic framework contains a full development of the real and complex numbers and of the rings of polynomials over these fields. The framework is constructive. It does not use anything apart from the Coq logic. The framework has been successfully used to formalize non-trivial mathematics as part of the FTA project.