CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Guarded Recursive Types in Type Theory

Andrea Vezzosi (Institutionen för data- och informationsteknik, Datavetenskap (Chalmers))
Göteborg : Chalmers University of Technology, 2015. - 63 s.

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 been challenging. Traditionally systems like Agda and Coq have relied on a syntactic restriction on (co)recursive calls, but this is inherently anti-modular. Guarded recursion, first introduced by Nakano, has been recently applied 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, using the proof assistant Agda, a result about strong normalization for a small 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.

Nyckelord: induction, coinduction, totality, type theory, guarded types, sized types, Agda

Denna post skapades 2015-11-20.
CPL Pubid: 226096


Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Datavetenskap (Chalmers)


Teoretisk datalogi

Chalmers infrastruktur


Datum: 2015-12-17
Tid: 13:15
Lokal: EDIT Building, room EE
Opponent: Conor McBride