| 1. |
- 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.
|
|
| 2. |
- 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.
|
|
| 3. |
- 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.
|
|
