An experimental library of formalized Mathematics based on the 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).

Download Full-text

Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention

Mathematical Structures in Computer Science ◽

10.1017/s0960129521000335 ◽

2021 ◽

pp. 1-20

Author(s):

Ernesto Copello ◽

Nora Szasz ◽

Álvaro Tasistro

Keyword(s):

Type Theory ◽

Lambda Calculus ◽

Proof Assistant ◽

First Order ◽

Constructive Type Theory ◽

Fundamental Part ◽

Constructive Type ◽

Free Variables ◽

The Church ◽

Theoretical Results

Abstarct We formalize in Constructive Type Theory the Lambda Calculus in its classical first-order syntax, employing only one sort of names for both bound and free variables, and with α-conversion based upon name swapping. As a fundamental part of the formalization, we introduce principles of induction and recursion on terms which provide a framework for reproducing the use of the Barendregt Variable Convention as in pen-and-paper proofs within the rigorous formal setting of a proof assistant. The principles in question are all formally derivable from the simple principle of structural induction/recursion on concrete terms. We work out applications to some fundamental meta-theoretical results, such as the Church–Rosser Theorem and Weak Normalization for the Simply Typed Lambda Calculus. The whole development has been machine checked using the system Agda.

Download Full-text

Homotopy limits in type theory

Mathematical Structures in Computer Science ◽

10.1017/s0960129514000498 ◽

2015 ◽

Vol 25 (5) ◽

pp. 1040-1070 ◽

Cited By ~ 11

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.

Download Full-text

Completeness theorems for first-order logic analysed in constructive type theory

Journal of Logic and Computation ◽

10.1093/logcom/exaa073 ◽

2021 ◽

Vol 31 (1) ◽

pp. 112-151

Author(s):

Yannick Forster ◽

Dominik Kirst ◽

Dominik Wehr

Keyword(s):

Type Theory ◽

Order Logic ◽

First Order Logic ◽

First Order ◽

Constructive Type Theory ◽

Constructive Type ◽

The Standard Model ◽

Coq Proof Assistant ◽

Game Theoretic ◽

Completeness Theorems

Abstract We study various formulations of the completeness of first-order logic phrased in constructive type theory and mechanised in the Coq proof assistant. Specifically, we examine the completeness of variants of classical and intuitionistic natural deduction and sequent calculi with respect to model-theoretic, algebraic, and game-theoretic semantics. As completeness with respect to the standard model-theoretic semantics à la Tarski and Kripke is not readily constructive, we analyse connections of completeness theorems to Markov’s Principle and Weak K̋nig’s Lemma and discuss non-standard semantics admitting assumption-free completeness. We contribute a reusable Coq library for first-order logic containing all results covered in this paper.

Download Full-text

A univalent formalization of the p-adic numbers

Mathematical Structures in Computer Science ◽

10.1017/s0960129514000541 ◽

2015 ◽

Vol 25 (5) ◽

pp. 1147-1171 ◽

Cited By ~ 2

Author(s):

ÁLVARO PELAYO ◽

VLADIMIR VOEVODSKY ◽

MICHAEL A. WARREN

Keyword(s):

Proof Assistant ◽

The Coq Proof Assistant ◽

Coq Proof Assistant ◽

Constructive Algebra ◽

Univalent Foundations

The goal of this paper is to report on a formalization of the p-adic numbers in the setting of the second author's univalent foundations program. This formalization, which has been verified in the Coq proof assistant, provides an approach to the p-adic numbers in constructive algebra and analysis.

Download Full-text

Verification of non-functional programs using interpretations in type theory

Journal of Functional Programming ◽

10.1017/s095679680200446x ◽

2003 ◽

Vol 13 (4) ◽

pp. 709-745 ◽

Cited By ~ 42

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.

Download Full-text