Generalization in Type Theory Based Proof Assistants

2002 ◽  
pp. 217-232 ◽  
Author(s):  
Olivier Pons
Keyword(s):  
Type Theory ◽  
Proof Assistants

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 MiniAgda: Integrating Sized and Dependent Types

10.29007/322q ◽  
2018 ◽  
Author(s):  
Andreas Abel
Keyword(s):  
Programming Languages ◽  
Type Theory ◽  
Type System ◽  
Proof Assistants ◽  
Parametric Function ◽  
Dependent Type Theory ◽  
Essential Idea ◽  
Core Language ◽  
Higher Order Functions ◽  
Dependent Type

Sized types are a modular and theoretically well-understood tool for checking termination of recursive and productivity of corecursive definitions. The essential idea is to track structural descent and guardedness in the type system to make termination checking robust and suitable for strong abstractions like higher-order functions and polymorphism.To study the application of sized types to proof assistants and programming languages based on dependent type theory, we have implemented a core language with explicit handling of sizes. New considerations were necessary to soundly integrate sized types with dependencies and pattern matching, which was made possible by modern concepts such as inaccessible patterns and parametric function spaces.

scholarly journals Denotational semantics for guarded dependent type theory

2020 ◽  
Vol 30 (4) ◽  
pp. 342-378
Author(s):  
Aleš Bizjak ◽  
Rasmus Ejlers Møgelberg
Keyword(s):  
Type Theory ◽  
Denotational Semantics ◽  
Dependent Types ◽  
Proof Assistants ◽  
New Model ◽  
Dependent Type Theory ◽  
Additional Requirement ◽  
The One ◽  
Dependent Type

AbstractWe present a new model of guarded dependent type theory (GDTT), a type theory with guarded recursion and multiple clocks in which one can program with and reason about coinductive types. Productivity of recursively defined coinductive programs and proofs is encoded in types using guarded recursion and can therefore be checked modularly, unlike the syntactic checks implemented in modern proof assistants. The model is based on a category of covariant presheaves over a category of time objects, and quantification over clocks is modelled using a presheaf of clocks. To model the clock irrelevance axiom, crucial for programming with coinductive types, types must be interpreted as presheaves internally right orthogonal to the object of clocks. In the case of dependent types, this translates to a lifting condition similar to the one found in homotopy theoretic models of type theory, but here with an additional requirement of uniqueness of lifts. Since the universes defined by the standard Hofmann–Streicher construction in this model do not satisfy this property, the universes in GDTT must be indexed by contexts of clock variables. We show how to model these universes in such a way that inclusions of clock contexts give rise to inclusions of universes commuting with type operations on the nose.

scholarly journals Homotopy theoretic models of identity types

2009 ◽  
Vol 146 (1) ◽  
pp. 45-55 ◽  
Author(s):  
STEVE AWODEY ◽  
MICHAEL A. WARREN
Keyword(s):  
Mathematical Logic ◽  
Type Theory ◽  
Theoretical Basis ◽  
Homotopy Theory ◽  
Model Category ◽  
Proof Assistants ◽  
Model Categories ◽  
Wide Range ◽  
Abstract Framework ◽  
Computer Proof

Quillen [17] introduced model categories as an abstract framework for homotopy theory which would apply to a wide range of mathematical settings. By all accounts this program has been a success and—as, e.g., the work of Voevodsky on the homotopy theory of schemes [15] or the work of Joyal [11,12] and Lurie [13] on quasicategories seem to indicate—it will likely continue to facilitate mathematical advances. In this paper we present a novel connection between model categories and mathematical logic, inspired by the groupoid model of (intensional) Martin–Löf type theory [14] due to Hofmann and Streicher [9]. In particular, we show that a form of Martin–Löf type theory can be soundly modelled in any model category. This result indicates moreover that any model category has an associated “internal language” which is itself a form of Martin-Löf type theory. This suggests applications both to type theory and to homotopy theory. Because Martin–Löf type theory is, in one form or another, the theoretical basis for many of the computer proof assistants currently in use, such asCoqandAgda(cf. [3] and [5]), this promise of applications is of a practical, as well as theoretical, nature.

Type Theory and Formal Proof

2009 ◽  
Author(s):  
Rob Nederpelt ◽  
Herman Geuvers
Keyword(s):  
Type Theory ◽  
Formal Proof

Computational Models for Multilayered Composite Shells with Application to Tires

1996 ◽  
Vol 24 (1) ◽  
pp. 11-38 ◽  
Author(s):  
G. M. Kulikov
Keyword(s):  
Type Theory ◽  
Computational Models ◽  
Geometrical Nonlinearity ◽  
Higher Order ◽  
Stress Strain ◽  
Strain Fields ◽  
First Order ◽  
Timoshenko Type ◽  
Joint Influence ◽  
Discrete Layer

Abstract This paper focuses on four tire computational models based on two-dimensional shear deformation theories, namely, the first-order Timoshenko-type theory, the higher-order Timoshenko-type theory, the first-order discrete-layer theory, and the higher-order discrete-layer theory. The joint influence of anisotropy, geometrical nonlinearity, and laminated material response on the tire stress-strain fields is examined. The comparative analysis of stresses and strains of the cord-rubber tire on the basis of these four shell computational models is given. Results show that neglecting the effect of anisotropy leads to an incorrect description of the stress-strain fields even in bias-ply tires.

Sign in / Sign up

Export Citation Format

Share Document