scholarly journals The Marriage of Univalence and Parametricity

2021 ◽  
Vol 68 (1) ◽  
pp. 1-44
Author(s):  
Nicolas Tabareau ◽  
Éric Tanter ◽  
Matthieu Sozeau
Keyword(s):  
Type Theory ◽  
Program Verification ◽  
Proof Assistants ◽  
Computationally Efficient ◽  
Lightweight Framework ◽  
The Coq Proof Assistant ◽  
Coq Proof Assistant ◽  
Efficient Representation ◽  
Term Dependency ◽  
Work First

Reasoning modulo equivalences is natural for everyone, including mathematicians. Unfortunately, in proof assistants based on type theory, which are frequently used to mechanize mathematical results and carry out program verification efforts, equality is appallingly syntactic, and as a result, exploiting equivalences is cumbersome at best. Parametricity and univalence are two major concepts that have been explored in the literature to transport programs and proofs across type equivalences, but they fall short of achieving seamless, automatic transport. This work first clarifies the limitations of these two concepts when considered in isolation and then devises a fruitful marriage between both. The resulting concept, called univalent parametricity , is an extension of parametricity strengthened with univalence that fully realizes programming and proving modulo equivalences. Our approach handles both type and term dependency, as well as type-level computation. In addition to the theory of univalent parametricity, we present a lightweight framework implemented in the Coq proof assistant that allows the user to transparently transfer definitions and theorems for a type to an equivalent one, as if they were equal. For instance, this makes it possible to conveniently switch between an easy-to-reason-about representation and a computationally efficient representation as soon as they are proven equivalent. The combination of parametricity and univalence supports transport à la carte : basic univalent transport, which stems from a type equivalence, can be complemented with additional proofs of equivalences between functions over these types, in order to be able to transport more programs and proofs, as well as to yield more efficient terms. We illustrate the use of univalent parametricity on several examples, including a recent integration of native integers in Coq. This work paves the way to easier-to-use proof assistants by supporting seamless programming and proving modulo equivalences.

scholarly journals Homotopy limits in type theory

2015 ◽  
Vol 25 (5) ◽  
pp. 1040-1070 ◽  
Author(s):  
JEREMY AVIGAD ◽  
KRZYSZTOF KAPULKIN ◽  
PETER LEFANU LUMSDAINE
Keyword(s):  
Homotopy Type ◽  
Systematic Study ◽  
Type Theory ◽  
Proof Assistant ◽  
Classical Approach ◽  
Homotopy Type Theory ◽  
The Coq Proof Assistant ◽  
Homotopy Limits ◽  
Coq Proof Assistant

Working in homotopy type theory, we provide a systematic study of homotopy limits of diagrams over graphs, formalized in the Coq proof assistant. We discuss some of the challenges posed by this approach to the formalizing homotopy-theoretic material. We also compare our constructions with the more classical approach to homotopy limits via fibration categories.

scholarly journals An experimental library of formalized Mathematics based on the univalent foundations

2015 ◽  
Vol 25 (5) ◽  
pp. 1278-1294 ◽  
Author(s):  
VLADIMIR VOEVODSKY
Keyword(s):  
Type Theory ◽  
Proof Assistant ◽  
Formalization Of Mathematics ◽  
Constructive Type Theory ◽  
Short Overview ◽  
Formalized Mathematics ◽  
The Coq Proof Assistant ◽  
Constructive Type ◽  
Coq Proof Assistant ◽  
Univalent Foundations

This is a short overview of an experimental library of Mathematics formalized in the Coq proof assistant using the univalent interpretation of the underlying type theory of Coq. I started to work on this library in February 2010 in order to gain experience with formalization of Mathematics in a constructive type theory based on the intuition gained from the univalent models (see Kapulkin et al. 2012).

scholarly journals Modular development of certified program verifiers with a proof assistant,

2008 ◽  
Vol 18 (5-6) ◽  
pp. 599-647 ◽  
Author(s):  
ADAM CHLIPALA
Keyword(s):  
Program Verification ◽  
Type System ◽  
Minimal Amount ◽  
Dependent Types ◽  
Proof Assistant ◽  
Machine Code ◽  
The Coq Proof Assistant ◽  
Verification Tool ◽  
Coq Proof Assistant ◽  
New Type

AbstractWe report on an experience using the Coq proof assistant to develop a program verification tool with a machine-checked proof of full correctness. The verifier is able to prove memory safety of x86 machine code programs compiled from code that uses algebraic datatypes. The tool's soundness theorem is expressed in terms of the bit-level semantics of x86 programs, so its correctness depends on very few assumptions. We take advantage of Coq's support for programming with dependent types and modules in the structure of the development. The approach is based on developing a library of reusable functors for transforming a verifier at one level of abstraction into a verifier at a lower level. Using this library, it is possible to prototype a verifier based on a new type system with a minimal amount of work, while obtaining a very strong soundness theorem about the final product.

scholarly journals EMTST: Engineering the Meta-theory of Session Types

2020 ◽  
pp. 278-285
Author(s):  
David Castro ◽  
Francisco Ferreira ◽  
Nobuko Yoshida
Keyword(s):  
Wide Spectrum ◽  
Type Systems ◽  
Small Scale ◽  
Proof Assistant ◽  
Proof Assistants ◽  
Type Safety ◽  
Session Types ◽  
The Coq Proof Assistant ◽  
Coq Proof Assistant ◽  
Type Preservation

Abstract Session types provide a principled programming discipline for structured interactions. They represent a wide spectrum of type-systems for concurrency. Their type safety is thus extremely important. EMTST is a tool to aid in representing and validating theorems about session types in the Coq proof assistant. On paper, these proofs are often tricky, and error prone. In proof assistants, they are typically long and difficult to prove. In this work, we propose a library that helps validate the theory of session types calculi in proof assistants. As a case study, we study two of the most used binary session types systems: we show the impossibility of representing the first system in $$\alpha $$-equivalent representations, and we prove type preservation for the revisited system. We develop our tool in the Coq proof assistant, using locally nameless for binders and small scale reflection to simplify the handling of linear typing environments.

Verification of non-functional programs using interpretations in type theory

2003 ◽  
Vol 13 (4) ◽  
pp. 709-745 ◽  
Author(s):  
JEAN-CHRISTOPHE FILLIÂTRE
Keyword(s):  
Static Analysis ◽  
Type Theory ◽  
General Framework ◽  
Specification Language ◽  
Proof Assistant ◽  
Logical Interpretation ◽  
Total Correctness ◽  
The Coq Proof Assistant ◽  
Coq Proof Assistant ◽  
Functional Features

We study the problem of certifying programs combining imperative and functional features within the general framework of type theory. Type theory is a powerful specification language which is naturally suited for the proof of purely functional programs. To deal with imperative programs, we propose a logical interpretation of an annotated program as a partial proof of its specification. The construction of the corresponding partial proof term is based on a static analysis of the effects of the program which excludes aliases. The missing subterms in the partial proof term are seen as proof obligations, whose actual proofs are left to the user. We show that the validity of those proof obligations implies the total correctness of the program. This work has been implemented in the Coq proof assistant. It appears as a tactic taking an annotated program as argument and generating a set of proof obligations. Several nontrivial algorithms have been certified using this tactic.

scholarly journals Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant

2006 ◽  
pp. 114-129 ◽  
Author(s):  
Gilles Barthe ◽  
Julien Forest ◽  
David Pichardie ◽  
Vlad Rusu
Keyword(s):  
Proof Assistant ◽  
Recursive Functions ◽  
The Coq Proof Assistant ◽  
Coq Proof Assistant ◽  
Practical Tool

scholarly journals Compact and Computationally Efficient Representation of Deep Neural Networks

2020 ◽  
Vol 31 (3) ◽  
pp. 772-785 ◽  
Author(s):  
Simon Wiedemann ◽  
Klaus-Robert Muller ◽  
Wojciech Samek
Keyword(s):  
Neural Networks ◽  
Deep Neural Networks ◽  
Computationally Efficient ◽  
Efficient Representation

scholarly journals Residual theory in λ-calculus: a formal development

1994 ◽  
Vol 4 (3) ◽  
pp. 371-394 ◽  
Author(s):  
Gérard Huet
Keyword(s):  
Normal Forms ◽  
Data Types ◽  
The Coq Proof Assistant ◽  
Coq Proof Assistant ◽  
Concrete Syntax ◽  
Calculus Of Inductive Constructions ◽  
Recursive Definitions ◽  
Abstract Framework ◽  
Order Predicate Calculus ◽  
Standard Library

AbstractWe present the complete development, in Gallina, of the residual theory of β-reduction in pure λ-calculus. The main result is the Prism Theorem, and its corollary Lévy's Cube Lemma, a strong form of the parallel-moves lemma, itself a key step towards the confluence theorem and its usual corollaries (Church-Rosser, uniqueness of normal forms). Gallina is the specification language of the Coq Proof Assistant (Dowek et al., 1991; Huet 1992b). It is a specific concrete syntax for its abstract framework, the Calculus of Inductive Constructions (Paulin-Mohring, 1993). It may be thought of as a smooth mixture of higher-order predicate calculus with recursive definitions, inductively defined data types and inductive predicate definitions reminiscent of logic programming. The development presented here was fully checked in the current distribution version Coq V5.8. We just state the lemmas in the order in which they are proved, omitting the proof justifications. The full transcript is available as a standard library in the distribution of Coq.

Sign in / Sign up

Export Citation Format

Share Document