| 1. |
- Abel, Andreas, 1974, et al.
(författare)
-
A formalized proof of strong normalization for guarded recursive types
- 2014
-
Ingår i: Lecture Notes in Computer Science: 12th Asian Symposium on Programming Languages and Systems, APLAS 2014 Singapore, 17-19 November 2014. - Cham : Springer International Publishing. - 0302-9743 .- 1611-3349. - 9783319127354 ; 8858, s. 140-158
-
Konferensbidrag (refereegranskat)abstract
- We consider a simplified version of Nakano’s guarded fixed-point types in a representation by infinite type expressions, defined coinductively. Smallstep reduction is parametrized by a natural number “depth” that expresses under how many guards we may step during evaluation. We prove that reduction is strongly normalizing for any depth. The proof involves a typed inductive notion of strong normalization and a Kripke model of types in two dimensions: depth and typing context. Our results have been formalized in Agda and serve as a case study of reasoning about a language with coinductive type expressions.
|
|
| 2. |
- Abel, Andreas, 1974, et al.
(författare)
-
Decidability of Conversion for Type Theory in Type Theory
- 2018
-
Ingår i: Proceedings of the ACM on Programming Languages. - : Association for Computing Machinery (ACM). - 2475-1421. ; 2:POPL, s. 23:1-23:29
-
Tidskriftsartikel (refereegranskat)abstract
- Type theory should be able to handle its own meta-theory, both to justify its foundational claims and to obtain a verified implementation. At the core of a type checker for intensional type theory lies an algorithm to check equality of types, or in other words, to check whether two types are convertible. We have formalized in Agda a practical conversion checking algorithm for a dependent type theory with one universe à la Russell, natural numbers, and η-equality for Π types. We prove the algorithm correct via a Kripke logical relation parameterized by a suitable notion of equivalence of terms. We then instantiate the parameterized fundamental lemma twice: once to obtain canonicity and injectivity of type formers, and once again to prove the completeness of the algorithm. Our proof relies on inductive-recursive definitions, but not on the uniqueness of identity proofs. Thus, it is valid in variants of intensional Martin-Löf Type Theory as long as they support induction-recursion, for instance, Extensional, Observational, or Homotopy Type Theory.
|
|
| 3. |
- Abel, Andreas, 1974, et al.
(författare)
-
Normalization by evaluation for sized dependent types
- 2017
-
Ingår i: Proceedings of the ACM on Programming Languages. - : Association for Computing Machinery (ACM). - 2475-1421. ; 1:ICFP, s. 33:1-33:30
-
Tidskriftsartikel (refereegranskat)abstract
- Sized types have been developed to make termination checking more perspicuous, more powerful, and more modular by integrating termination into type checking. In dependently-typed proof assistants where proofs by induction are just recursive functional programs, the termination checker is an integral component of the trusted core, as validity of proofs depend on termination. However, a rigorous integration of full-fledged sized types into dependent type theory is lacking so far. Such an integration is non-trivial, as explicit sizes in proof terms might get in the way of equality checking, making terms appear distinct that should have the same semantics. In this article, we integrate dependent types and sized types with higher-rank size polymorphism, which is essential for generic programming and abstraction. We introduce a size quantifier (\forall) which lets us ignore sizes in terms for equality checking, alongside with a second quantifier Î for abstracting over sizes that do affect the semantics of types and terms. Judgmental equality is decided by an adaptation of normalization-by-evaluation for our new type theory, which features type shape-directed reflection and reification. It follows that subtyping and type checking of normal forms are decidable as well, the latter by a bidirectional algorithm.
|
|
| 4. |
- Ahn, Ki Yung, et al.
(författare)
-
Executable relational specifications of polymorphic type systems using prolog
- 2016
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. - 9783319296036 ; 9613, s. 109-125
-
Konferensbidrag (refereegranskat)abstract
- A concise, declarative, and machine executable specification of the Hindley–Milner type system (HM) can be formulated using logic programming languages such as Prolog. Modern functional language implementations such as the Glasgow Haskell Compiler support more extensive flavors of polymorphism beyond Milner’s theory of type polymorphism in the late 70's. We progressively extend the HM specification to include more advanced type system features. An interesting development is that extending dimensions of polymorphism beyond HM resulted in a multi-staged solution: resolve the typing relations first, while delaying to resolve kinding relations, and then resolve the delayed kinding relations. Our work demonstrates that logic programing is effective for prototyping polymorphic type systems with rich features of polymorphism, and that logic programming could have been even more effective for specifying type inference if it were equipped with better theories and tools for staged resolution of different relations at different levels.
|
|
| 5. |
- Axelsson, Emil, 1978, et al.
(författare)
-
Lightweight Higher-Order Rewriting in Haskell
- 2015
-
Ingår i: Trends in Functional Programming.
-
Konferensbidrag (övrigt vetenskapligt/konstnärligt)abstract
- We present a generic Haskell library for expressing rewrite rules with a safe treatment of variables and binders. Both sides of the rules are written as typed EDSL expressions, which leads to syntactically appealing rules and hides the underlying term representation. Matching is defined as an instance of Miller's pattern unification, which makes for efficient execution when rules are applied in a bottom-up fashion. The restrictions of pattern unification are captured in the types of the library, and we show by example that the library is capable of expressing useful simplifications that might be used in a compiler.
|
|
| 6. |
- Axelsson, Emil, 1978, et al.
(författare)
-
Lightweight Higher-Order Rewriting in Haskell
- 2016
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 9547, s. 1-21
-
Konferensbidrag (refereegranskat)abstract
- We present a generic Haskell library for expressing rewrite rules with a safe treatment of variables and binders. Both sides of the rules are written as typed EDSL expressions, which leads to syntactically appealing rules and hides the underlying term representation. Matching is defined as an instance of Miller's higher-order pattern unification and has the same complexity as first-order matching. The restrictions of pattern unification are captured in the types of the library, and we show by example that the library is capable of expressing useful simplifications that might be used in a compiler.
|
|
| 7. |
- Birkedal, Lars, et al.
(författare)
-
Guarded Cubical Type Theory
- 2019
-
Ingår i: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 63:2, s. 211-253
-
Tidskriftsartikel (refereegranskat)abstract
- This paper improves the treatment of equality in guarded dependent type theory ((Formula presented.)), by combining it with cubical type theory ((Formula presented.)). (Formula presented.) is an extensional type theory with guarded recursive types, which are useful for building models of program logics, and for programming and reasoning with coinductive types. We wish to implement (Formula presented.) with decidable type checking, while still supporting non-trivial equality proofs that reason about the extensions of guarded recursive constructions. (Formula presented.) is a variation of Martin–Löf type theory in which the identity type is replaced by abstract paths between terms. (Formula presented.) provides a computational interpretation of functional extensionality, enjoys canonicity for the natural numbers type, and is conjectured to support decidable type-checking. Our new type theory, guarded cubical type theory ((Formula presented.)), provides a computational interpretation of extensionality for guarded recursive types. This further expands the foundations of (Formula presented.) as a basis for formalisation in mathematics and computer science. We present examples to demonstrate the expressivity of our type theory, all of which have been checked using a prototype type-checker implementation. We show that (Formula presented.) can be given semantics in presheaves on (Formula presented.), where (Formula presented.) is the cube category, and (Formula presented.) is any small category with an initial object. We then show that the category of presheaves on (Formula presented.) provides semantics for (Formula presented.).
|
|
| 8. |
- Birkedal, Lars, et al.
(författare)
-
Guarded Cubical Type Theory: Path Equality for Guarded Recursion
- 2016
-
Ingår i: Leibniz International Proceedings in Informatics, LIPIcs. - 1868-8969. - 9783959770224 ; 62, s. 23:1-23:17
-
Konferensbidrag (refereegranskat)abstract
- This paper improves the treatment of equality in guarded dependent type theory (GDTT), by combining it with cubical type theory (CTT). GDTT is an extensional type theory with guarded recursive types, which are useful for building models of program logics, and for programming and reasoning with coinductive types. We wish to implement GDTT with decidable type checking, while still supporting non-trivial equality proofs that reason about the extensions of guarded recursive constructions. CTT is a variation of Martin-Löf type theory in which the identity type is replaced by abstract paths between terms. CTT provides a computational interpretation of functional extensionality, is conjectured to have decidable type checking, and has an implemented type checker. Our new type theory, called guarded cubical type theory, provides a computational interpretation of extensionality for guarded recursive types. This further expands the foundations of CTT as a basis for formalisation in mathematics and computer science. We present examples to demonstrate the expressivity of our type theory, all of which have been checked using a prototype type-checker implementation, and present semantics in a presheaf category.
|
|
| 9. |
- Capriotti, Paolo, et al.
(författare)
-
Functions out of Higher Truncations
- 2015
-
Ingår i: Leibniz International Proceedings in Informatics, LIPIcs. - 1868-8969. - 9783939897903 ; 41, s. 359-373
-
Konferensbidrag (refereegranskat)abstract
- In homotopy type theory, the truncation operator ||-||n (for a number n greater or equal to -1) is often useful if one does not care about the higher structure of a type and wants to avoid coherence problems. However, its elimination principle only allows to eliminate into n-types, which makes it hard to construct functions ||A||n -> B if B is not an n-type. This makes it desirable to derive more powerful elimination theorems. We show a first general result: If B is an (n+1)-type, then functions ||A||n -> B correspond exactly to functions A -> B that are constant on all (n+1)-st loop spaces. We give one "elementary" proof and one proof that uses a higher inductive type, both of which require some effort. As a sample application of our result, we show that we can construct "set-based" representations of 1-types, as long as they have "braided" loop spaces. The main result with one of its proofs and the application have been formalised in Agda.
|
|
| 10. |
- Nuyts, Andreas, et al.
(författare)
-
Parametric quantifiers for dependent type theory
- 2017
-
Ingår i: Proceedings of the ACM on Programming Languages. - : Association for Computing Machinery (ACM). - 2475-1421. ; 1:ICFP, s. 32:1--32:29-
-
Tidskriftsartikel (refereegranskat)abstract
- Polymorphic type systems such as System F enjoy the parametricity property: polymorphic functions cannot inspect their type argument and will therefore apply the same algorithm to any type they are instantiated on. This idea is formalized mathematically in Reynolds's theory of relational parametricity, which allows the metatheoretical derivation of parametricity theorems about all values of a given type. Although predicative System F embeds into dependent type systems such as Martin-Löf Type Theory (MLTT), parametricity does not carry over as easily. The identity extension lemma, which is crucial if we want to prove theorems involving equality, has only been shown to hold for small types, excluding the universe. We attribute this to the fact that MLTT uses a single type former Π to generalize both the parametric quantifier ∀ and the type former → which is non-parametric in the sense that its elements may use their argument as a value. We equip MLTT with parametric quantifiers ∀ and ∃ alongside the existing Π and Σ, and provide relation type formers for proving parametricity theorems internally. We show internally the existence of initial algebras and final co-algebras of indexed functors both by Church encoding and, for a large class of functors, by using sized types. We prove soundness of our type system by enhancing existing iterated reflexive graph (cubical set) models of dependently typed parametricity by distinguishing between edges that express relatedness of objects (bridges) and edges that express equality (paths). The parametric functions are those that map bridges to paths. We implement an extension to the Agda proof assistant that type-checks proofs in our type system.
|
|
| 11. |
- Nuyts, Andreas, et al.
(författare)
-
Parametric quantifiers for dependent types
- 2017
-
Ingår i: Leibniz International Proceedings in Informatics, LIPIcs. - 1868-8969. ; 104, s. 83-84
-
Konferensbidrag (refereegranskat)
|
|
| 12. |
- Sattler, Christian, 1988, et al.
(författare)
-
Partial Univalence in n-truncated Type Theory
- 2020
-
Ingår i: ACM International Conference Proceeding Series. - New York, NY, USA : ACM. ; , s. 807-819
-
Konferensbidrag (refereegranskat)abstract
- It is well known that univalence is incompatible with uniqueness of identity proofs (UIP), the axiom that all types are h-sets. This is due to finite h-sets having non-trivial automorphisms as soon as they are not h-propositions. A natural question is then whether univalence restricted to h-propositions is compatible with UIP. We answer this affirmatively by constructing a model where types are elements of a closed universe defined as a higher inductive type in homotopy type theory. This universe has a path constructor for simultaneous "partial" univalent completion, i.e., restricted to h-propositions. More generally, we show that univalence restricted to (n-1)-types is consistent with the assumption that all types are n-truncated. Moreover we parametrize our construction by a suitably well-behaved container, to abstract from a concrete choice of type formers for the universe.
|
|
| 13. |
- Vezzosi, Andrea, 1986
(författare)
-
Guarded Recursive Types in Type Theory
- 2015
-
Licentiatavhandling (övrigt vetenskapligt/konstnärligt)abstract
- In total functional (co)programming valid programs are guaranteed to always produce (part of) their output in a finite number of steps.Enforcing this property while not sacrificing expressivity has beenchallenging. Traditionally systems like Agda and Coq have relied on a syntactic restriction on (co)recursive calls, but this is inherentlyanti-modular.Guarded recursion, first introduced by Nakano, has been recentlyapplied in the coprogramming case to ensure totality through typing instead. The relationship between the consumption and the production of data is captured by a delay modality, which allows to give a safe type to a general fixpoint combinator.This thesis consists of two parts. In the first we formalize, usingthe proof assistant Agda, a result about strong normalization for asmall language extended with guarded recursive types. In the second we extend guarded recursive types to additionally ensure termination of recursive programs: the main result is a model based on relational parametricity for the dependently typed calculus we designed.
|
|
| 14. |
- Vezzosi, Andrea, 1986
(författare)
-
On Induction, Coinduction and Equality in Martin-Löf and Homotopy Type Theory
- 2018
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Martin Löf Type Theory, having put computation at the center of logical reasoning, has been shown to be an effective foundation for proof assistants, with applications both in computer science and constructive mathematics. One ambition though is for MLTT to also double as a practical general purpose programming language. Datatypes in type theory come with an induction or coinduction principle which gives a precise and concise specification of their interface. However, such principles can interfere with how we would like to express our programs. In this thesis, we investigate more flexible alternatives to direct uses of the (co)induction principles. As a first contribution, we consider the n-truncation of a type in Homo- topy Type Theory. We derive in HoTT an eliminator into (n+1)-truncated types instead of n-truncated ones, assuming extra conditions on the underlying function. As a second contribution, we improve on type-based criteria for termination and productivity. By augmenting the types with well-foundedness information, such criteria allow function definitions in a style closer to general recursion. We consider two criteria: guarded types, and sized types. Guarded types introduce a modality ”later” to guard the availability of recursive calls provided by a general fixed-point combinator. In Guarded Cu- bical Type Theory we equip the fixed-point combinator with a propositional equality to its one-step unfolding, instead of a definitional equality that would break normalization. The notion of path from Cubical Type Theory allows us to do so without losing canonicity or decidability of conversion. Sized types, on the other hand, explicitly index datatypes with size bounds on the height or depth of their elements. The sizes however can get in the way of the reasoning principles we expect. Our approach is to introduce new quantifiers for ”irrelevant” size quantification. We present a type theory with parametric quantifiers where irrelevance arises as a “free theorem”. We also develop a conversion checking algorithm for a more specific theory where the new quantifiers are restricted to sizes. Finally, our third contribution is about the operational semantics of type theory. For the extensions above we would like to devise a practical conversion checking algorithm suitable for integration into a proof assistant. We formal- ized the correctness of such an algorithm for a small but challenging core calculus, proving that conversion is decidable. We expect this development to form a good basis to verify more complex theories. The ideas discussed in this thesis are already influencing the development of Agda, a proof assistant based on type theory.
|
|
