Denotational semantics of recursive types in synthetic guarded domain theory

Just like any other branch of mathematics, denotational semantics of programming languages should be formalised in type theory, but adapting traditional domain theoretic semantics, as originally formulated in classical set theory to type theory has proven challenging. This paper is part of a project on formulating denotational semantics in type theories with guarded recursion. This should have the benefit of not only giving simpler semantics and proofs of properties such as adequacy, but also hopefully in the future to scale to languages with advanced features, such as general references, outside the reach of traditional domain theoretic techniques.Working inGuarded Dependent Type Theory(GDTT), we develop denotational semantics for Fixed Point Calculus (FPC), the simply typed lambda calculus extended with recursive types, modelling the recursive types of FPC using the guarded recursive types ofGDTT. We prove soundness and computational adequacy of the model inGDTTusing a logical relation between syntax and semantics constructed also using guarded recursive types. The denotational semantics is intensional in the sense that it counts the number of unfold-fold reductions needed to compute the value of a term, but we construct a relation relating the denotations of extensionally equal terms, i.e., pairs of terms that compute the same value in a different number of steps. Finally, we show how the denotational semantics of terms can be executed inside type theory and prove that executing the denotation of a boolean term computes the same value as the operational semantics of FPC.

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

Logical Relations as Types: Proof-Relevant Parametricity for Program Modules

Journal of the ACM ◽

10.1145/3474834 ◽

2021 ◽

Vol 68 (6) ◽

pp. 1-47

Author(s):

Jonathan Sterling ◽

Robert Harper

Keyword(s):

Type Theory ◽

Practical Importance ◽

Language Design ◽

Synthetic Approach ◽

Logical Relation ◽

Dependent Type Theory ◽

Dynamic Programs ◽

Phase Sensitive ◽

Program Modules ◽

Dependent Type

The theory of program modules is of interest to language designers not only for its practical importance to programming, but also because it lies at the nexus of three fundamental concerns in language design: the phase distinction , computational effects , and type abstraction . We contribute a fresh “synthetic” take on program modules that treats modules as the fundamental constructs, in which the usual suspects of prior module calculi (kinds, constructors, dynamic programs) are rendered as derived notions in terms of a modal type-theoretic account of the phase distinction. We simplify the account of type abstraction (embodied in the generativity of module functors) through a lax modality that encapsulates computational effects, placing projectibility of module expressions on a type-theoretic basis. Our main result is a (significant) proof-relevant and phase-sensitive generalization of the Reynolds abstraction theorem for a calculus of program modules, based on a new kind of logical relation called a parametricity structure . Parametricity structures generalize the proof-irrelevant relations of classical parametricity to proof- relevant families, where there may be non-trivial evidence witnessing the relatedness of two programs—simplifying the metatheory of strong sums over the collection of types, for although there can be no “relation classifying relations,” one easily accommodates a “family classifying small families.” Using the insight that logical relations/parametricity is itself a form of phase distinction between the syntactic and the semantic, we contribute a new synthetic approach to phase separated parametricity based on the slogan logical relations as types , by iterating our modal account of the phase distinction. We axiomatize a dependent type theory of parametricity structures using two pairs of complementary modalities (syntactic, semantic) and (static, dynamic), substantiated using the topos theoretic Artin gluing construction. Then, to construct a simulation between two implementations of an abstract type, one simply programs a third implementation whose type component carries the representation invariant.

Download Full-text

Observational equality: now for good

Proceedings of the ACM on Programming Languages ◽

10.1145/3498693 ◽

2022 ◽

Vol 6 (POPL) ◽

pp. 1-27

Author(s):

Loïc Pujet ◽

Nicolas Tabareau

Keyword(s):

Type Theory ◽

Identity Relation ◽

Logical Relation ◽

Type Checking ◽

Dependent Type Theory ◽

Proper Extension ◽

New Type ◽

Recent Extension ◽

Dependent Type

Building on the recent extension of dependent type theory with a universe of definitionally proof-irrelevant types, we introduce TTobs, a new type theory based on the setoidal interpretation of dependent type theory. TTobs equips every type with an identity relation that satisfies function extensionality, propositional extensionality, and definitional uniqueness of identity proofs (UIP). Compared to other existing proposals to enrich dependent type theory with these principles, our theory features a notion of reduction that is normalizing and provides an algorithmic canonicity result, which we formally prove in Agda using the logical relation framework of Abel et al. Our paper thoroughly develops the meta-theoretical properties of TTobs, such as the decidability of the conversion and of the type checking, as well as consistency. We also explain how to extend our theory with quotient types, and we introduce a setoidal version of Swan's Id types that turn it into a proper extension of MLTT with inductive equality.

Download Full-text