ABSTRACT. (Joint work with Carlo Angiuli, Evan Cavallo, Robert Harper and Jonathan Sterling)

Recent research revealed the deep connection between type theory and homotopy theory, which inspired a series of new type theories. The characteristic new features are univalence and higher inductive types, which have led to a fruitful development of synthetic homotopy theory. Unfortunately, those new features were originally introduced as axioms and disrupted the computational content of type theory, which affects their practicality in mechanizing proofs.

To date, the most promising approach to enjoy new features inspired by homotopy theory while retaining computational content is through cubical structure. Cohen et al. constructed a type theory based on De Morgan cubes with both univalence and higher inductive types. Influenced by their work, we also built a type-theoretic semantics with all the features, but instead based on Cartesian cubes. In addition to using a different cubical structure, our semantics is built from computational content directly, following a computation-first methodology which itself is interesting.

RedPRL is our first proof assistant based on the new semantics, inheriting the PRL style pioneered by the Nuprl proof assistant, which is also based on the computation-first methodology (but without cubical structure). We are also developing different proof assistants with distinct proof theories, in hope to create the best tools for mechanizing homotopy theory and other mathematics.

In this talk, I will describe how the computation-first methodology works, compare two cubical type theories and discuss RedPRL.

ABSTRACT. We observe today a large diversity of proof systems. This diversity has the negative consequence that a lot of theorems are proved many times. Unlike programming languages, it is difficult for these systems to co-operate because they do not implement the same logic. Logical frameworks are a class of theorem provers that overcome this issue by their capacity of implementing various logics. In this work, we study the STT∀ βδ logic, an extension of Simple Type Theory that has been encoded in the logical framework Dedukti. We present a translation from this logic to OpenTheory, a proof system and interoperability tool between provers of the HOL family. We have used this translation to export an arithmetic library containing Fermat’s little theorem to OpenTheory and to two other proof systems that are Coq and Matita.

ABSTRACT. The K framework was born from our firm belief that an ideal language framework is possible. Specifically, that programming languages must have formal definitions, and that tools for a given language, such as interpreters, compilers, state-space explorers, model checkers, deductive program verifiers, etc., are derived from just one reference formal definition of the language, correct-by-construction and at no additional cost specific to that language. No other semantics for the same language should be needed. Several real languages have been formalized their semantics in K, including C, Java, JavaScript, PHP, Python, Rust, and more recently the Etherem VM (EVM), and the generic K tools have been instantiated to with these languages. In particular, the EVM semantics is used commercially by Runtime Verification to formally verify smart contracts on the Ethereum blockchain. But what is behind K? Why and how does it work? This talk will discuss the logical formalism underlying K, matching logic, a first-order logic (FOL) variant for specifying and reasoning about structure by means of patterns and pattern matching. Matching logic generalizes several logical frameworks important for program analysis, such as: propositional logic, algebraic specification, FOL with equality, (polyadic) modal logics, temporal logics, separation logic, as well as dynamic and Hoare logics. Binders and fixed-points can also be defined in matching logic, and thus the variety of lambda/mu-calculi and substitution-based semantics. Patterns can specify both structural requirements, including separation requirements at any level in any program configuration (not only in the "heap"), as well as logical requirements and constraints. The various languages defined in K, regardless of their size and complexity, become nothing but matching logic theories, and the various tools provided by the K framework, such as interpretion, symbolic execution, search and model checking, as well as full-fledged deductive program verification, become nothing but proof search heuristics in matching logic.

ABSTRACT. The Abella theorem prover is based on a logic in which relations, and not functions, are defined by induction (and coinduction). Of course, many relations do, in fact, define functions and there is real value in separating functional computation (marked by determinism) from more general deduction (marked by nondeterminism and backtracking). Recent work on focused proof systems for the logic underlying Abella is used in this paper to motivate the design of various extensions to the Abella system. With these extensions to the system (which do not extend the logic), it is possible to fully automate functional computations within the relational setting as soon as a proof is provided that a given relation does, in fact, capture a total function. In this way, we can use Abella to compute functions on data structures that contain bindings.

ABSTRACT. Contrary to Dijkstra's diktat, testing, and more in general, validation, has found an increasing niche in formal verification, prior or even in alternative to theorem proving. Validation, and in particular, property-based testing (PBT) is quite effective in mechanized meta-theory of programming languages, where theorems have shallow but tedious proofs that may go wrong for fairly banal mistakes in specifications. In this report, we abandon the comfort of high-level object languages and address the validation of abstract machines and typed assembly languages. We concentrate on Appel and Leroy's List-machine benchmark (JAR, 2012), which we tackle both with alphaCheck, the simple model-checker on top of the nominal logic programming alphaProlog and the PBT library FSCheck for F#. This allows us to compare the relative merits of exhaustive-based PBT in a logic programming style versus the more usual randomized functional setting. We uncover one major bug in the published version of the paper, plus several typos and ambiguities thereof. This is particularly striking, as the paper is accompanied by two full formalizations, in Coq and Twelf. Finally, we do a bit of mutation testing on the given model, to asses further the trade-off between exhaustive and randomized data generation. Spoiler alert: the former performs better.

ABSTRACT. We present a full formalization in Martin-L\"of's Constructive Type Theory of the Standardization Theorem for the Lambda Calculus using first-order syntax with one sort of names for both free and bound variables and Stoughton's multiple substitution. Our version is based on a proof by Ryo Kashima, in which a notion of $\beta$-reducibility with a standard sequence is captured by an inductive relation. The proof uses only structural induction over the syntax and the relations defined, which is possible due to the specific formulation of substitution that we employ. The whole development has been machine-checked using the system Agda.

ABSTRACT. We introduce a universe of regular datatypes with variable binding information, for which we define generic formation, elimination, and induction operators. We then define a generic $\alpha$-equivalence relation over the types of the universe based on name-swapping, and derive iteration and induction principles which work modulo $\alpha$-conversion capturing Barendregt's Variable Convention. We instantiate the resulting framework so as to obtain the $\lambda$-Calculus and System F, for which we derive substitution operations and substitution lemmas for $\alpha$-conversion and substitution composition. The whole work is carried out in Constructive Type Theory and machine-checked by the system Agda.

ABSTRACT. Following the introduction of BNF notation by Backus for the Algol 60 report and subsequent notational variants, a metalanguage involving formal “grammars” has developed for discussing structured objects in Computer Science and Mathematical Logic. We refer to this offspring of BNF as Math-BNF or MBNF, to the original BNF and its notational variants just as BNF, and to aspects common to both as BNF-style. MBNF is sometimes called abstract syntax, but we avoid that name because MBNF is in fact a concrete form and has a more abstract form. What all BNF-style notations share is the use of production rules roughly of this form: ◯ ⩴ □₁ | ⋯ | □ₙ Normally, such a rule says “every instance of □ᵢ for i ∈ {1, ..., n} is also an instance of ◯”.

MBNF is distinct from BNF in the entities and operations it allows. Instead of strings, MBNF builds arrangements of symbols that we call math-text. Sometimes “syntax” is defined by interleaving MBNF production rules and other mathematical definitions that can contain chunks of math-text.

There is no clear definition of MBNF. Readers do not have a document which tells them how MBNF is to be read and must learn MBNF through a process of cultural initiation. To the extent that MBNF is defined, it is largely through examples scattered throughout the literature.

This paper gives MBNF examples illustrating some of the differences between MBNF and BNF. We propose a definition of syntactic math text (SMT) which handles many (but far from all) uses of math-text and MBNF in the wild. We aim to balance the goal of being accessible and not requiring too much prerequisite knowledge with the conflicting goal of providing a rich mathematical structure that already supports many uses and has possibilities to be extended to support more challenging cases.

ABSTRACT. Call-by-need is a lazy evaluation strategy which overwrites an argument with its value the first time it is evaluated, thus avoiding a costly re-evaluation mechanism. It is used in functional programming languages like Haskell and Miranda. In this talk we present a fresh view of call-by-need in three different aspects:

We revisit the completeness theorem relating (weak) call-by-need with standard (weak) call-by-name. We relate the syntactical notion of (weak) call-by-need with the corresponding semantical notion of (weak) neededness, based on the theory of residuals. We extend the weak call-by-need strategy, which only computes weak head normal forms of closed terms, to a strong call-by-need strategy which computes strong normal forms of open terms, a notion of reduction which is used in proof assistants like Coq and Agda.

We conclude our talk by proposing some future research directions.

ABSTRACT. The Bindlib library for OCaml provides a set of tools for the manipulation of data structures with variable binding. It is very well suited for the representation of abstract syntax trees, and has already been used for the implementation of half a dozen languages and proof assistants (including a new version of the logical framework Dedukti). Bindlib is optimised for fast substitution, and it supports variable renaming. Since the representation of binders is based on higher-order abstract syntax, variable capture cannot arise during substitution. As a consequence, variable names are not updated at substitution time. They can however be explicitly recomputed to avoid “visual capture” (i.e., distinct variables with the same apparent name) when a data structure is displayed.

ABSTRACT. In this progress report, we highlight the design of the functional programming language MLTS which we have recently proposed elsewhere. This language uses the λ-tree syntax approach to encoding data structures that contain bindings. In this setting, bound variables never become free nor escape their scope: instead, binders in data structures are permitted to move into binding sites within programs. The concrete syntax of MLTS is based on the one for OCaml but includes additional binders within programs that directly support the mobility of bindings. The natural semantics of MLTS can be viewed as a logical theory within the logic G, which forms the basis of the Abella proof system and which includes nominal abstractions and the ∇-quantifier. Here, we provide several examples of MLTS programs. We also illustrate how many Abella relational specifications that are known to specify functions can be rewritten as functions in MLTS.