Algebra of programming in Agda: Dependent types for relational program derivation

AbstractRelational program derivation is the technique of stepwise refining a relational specification to a program by algebraic rules. The program thus obtained is correct by construction. Meanwhile, dependent type theory is rich enough to express various correctness properties to be verified by the type checker. We have developed a library, AoPA (Algebra of Programming in Agda), to encode relational derivations in the dependently typed programming language Agda. A program is coupled with an algebraic derivation whose correctness is guaranteed by the type system. Two non-trivial examples are presented: an optimisation problem and a derivation of quicksort in which well-founded recursion is used to model terminating hylomorphisms in a language with inductive types.

Download Full-text

Cubical Agda: A dependently typed programming language with univalence and higher inductive types

Journal of Functional Programming ◽

10.1017/s0956796821000034 ◽

2021 ◽

Vol 31 ◽

Author(s):

ANDREA VEZZOSI ◽

ANDERS MÖRTBERG ◽

ANDREAS ABEL

Keyword(s):

Programming Language ◽

Type Theory ◽

Type Checking ◽

Dependent Type Theory ◽

Wide Range ◽

General Schema ◽

Direct Definition ◽

Inductive Types ◽

Definition Of ◽

Cubical Type Theory

Abstract Proof assistants based on dependent type theory provide expressive languages for both programming and proving within the same system. However, all of the major implementations lack powerful extensionality principles for reasoning about equality, such as function and propositional extensionality. These principles are typically added axiomatically which disrupts the constructive properties of these systems. Cubical type theory provides a solution by giving computational meaning to Homotopy Type Theory and Univalent Foundations, in particular to the univalence axiom and higher inductive types (HITs). This paper describes an extension of the dependently typed functional programming language Agda with cubical primitives, making it into a full-blown proof assistant with native support for univalence and a general schema of HITs. These new primitives allow the direct definition of function and propositional extensionality as well as quotient types, all with computational content. Additionally, thanks also to copatterns, bisimilarity is equivalent to equality for coinductive types. The adoption of cubical type theory extends Agda with support for a wide range of extensionality principles, without sacrificing type checking and constructivity.

Download Full-text

Introduction to the Special Issue on Dependent Type Theory Meets Practical Programming

Journal of Functional Programming ◽

10.1017/s0956796803004866 ◽

2004 ◽

Vol 14 (1) ◽

pp. 1-2

Author(s):

GILLES BARTHE ◽

PETER DYBJEN ◽

PETER THIEMANN

Keyword(s):

Programming Languages ◽

Type Theory ◽

Type System ◽

Type Systems ◽

Special Issue ◽

Dependent Type Theory ◽

Dependent Type

Download Full-text

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.

Download Full-text

Denotational semantics for guarded dependent type theory

Mathematical Structures in Computer Science ◽

10.1017/s0960129520000080 ◽

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.

Download Full-text

Special issue on Dependent Type Theory Meets Programming Practice CALL FOR PAPERS

Journal of Functional Programming ◽

10.1017/s0956796801004105 ◽

2001 ◽

Vol 11 (4) ◽

pp. 437-437

Author(s):

Gilles Barthe ◽

Peter Dybjer ◽

Peter Thiemann

Keyword(s):

Programming Languages ◽

Type Theory ◽

Type System ◽

Type Systems ◽

Point Of View ◽

Theoretical Point ◽

Special Issue ◽

Dependent Type Theory ◽

The Impact ◽

Dependent Type

Modern programming languages rely on advanced type systems that detect errors at compile-time. While the benefits of type systems have long been recognized, there are some areas where the standard systems in programming languages are not expressive enough. Language designers usually trade expressiveness for decidability of the type system. Some interesting programs will always be rejected (despite their semantical soundness) or be assigned uninformative types.There are several remedies to this situation. Dependent type systems, which allow the formation of types that explicitly depend on other types or values, are one of the most promising approaches. These systems are well-investigated from a theoretical point of view by logicians and type theorists. For example, dependent types are used in proof assistants to implement various logics and there are sophisticated proof editors for developing programs in a dependently typed language.To the present day, the impact of these developments on practical programming has been small, partially because of the level of sophistication of these systems and of their type checkers. Only recently, there have been efforts to integrate dependent systems into intermediate languages in compilers and programming languages. Additional uses have been identified in high-profile applications such as mobile code security, where terms of a dependently typed lambda calculus to encode safety proofs.A special issue of the Journal of Functional Programming will be devoted to the interplay between dependent type theory and programming practice. We welcome technical contributions in the field, as well as position papers that:[bull ] make researchers in programming languages aware of new developments and research directions on the theory side;[bull ] point out to theorists practical uses of advanced type systems and urge them to address theoretical problems arising in emerging applications.Authors who are concerned about the appropriateness of a topic are welcome to contact the guest editors. Manuscripts should be unpublished works and not submitted elsewhere. Revised and enhanced versions of papers published in conference proceedings that have not appeared in archival journals are eligible for submission. All submissions will be reviewed according to the usual standards of scholarship and originality.Submissions should be sent to Gilles Barthe ([email protected]), with a copy to Nasreen Ahmad ([email protected]). Submitted articles should be sent in postscript format, preferably gzipped and uuencoded. In addition, please send, as plain text, title, abstract and contact information.The submission deadline is December 1st, 2001.

Download Full-text

Constructing Infinitary Quotient-Inductive Types

Lecture Notes in Computer Science - Foundations of Software Science and Computation Structures ◽

10.1007/978-3-030-45231-5_14 ◽

2020 ◽

pp. 257-276

Author(s):

Marcelo P. Fiore ◽

Andrew M. Pitts ◽

S. C. Steenkamp

Keyword(s):

Type Theory ◽

Theorem Prover ◽

Dependent Type Theory ◽

Inductive Definitions ◽

Inductive Types ◽

Recursive Definitions ◽

Dependent Type

AbstractThis paper introduces an expressive class of quotient-inductive types, called QW-types. We show that in dependent type theory with uniqueness of identity proofs, even the infinitary case of QW-types can be encoded using the combination of inductive-inductive definitions involving strictly positive occurrences of Hofmann-style quotient types, and Abel’s size types. The latter, which provide a convenient constructive abstraction of what classically would be accomplished with transfinite ordinals, are used to prove termination of the recursive definitions of the elimination and computation properties of our encoding of QW-types. The development is formalized using the Agda theorem prover.

Download Full-text