Wed 20 Jan 2016 10:55 - 11:20 at Grand Bay South - Track 2: Types and Foundations Chair(s): Robert Atkey
We present an internal formalisation of dependent type theory in type theory using a special case of higher inductive types from Homotopy Type Theory which we call quotient inductive types (QITs). Our formalisation of type theory avoids refering to preterms or a typability relation but defines directly well typed objects by an inductive definition. We use the elimination principle to define the set-theoretic and logical predicate interpretation. The work has been formalized using the Agda system extended with QITs using postulates.
| Poster (poster.pdf) | 113KiB |
Wed 20 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Wed 20 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change
10:30 - 12:10 | Track 2: Types and FoundationsResearch Papers at Grand Bay South Chair(s): Robert Atkey University of Strathclyde | ||
10:30 25mTalk | Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega Research Papers Media Attached File Attached | ||
10:55 25mTalk | Type Theory in Type Theory using Quotient Inductive Types Research Papers Media Attached File Attached | ||
11:20 25mTalk | System Fω with Equirecursive Types for Datatype-generic Programming Research Papers Yufei Cai University of Tübingen, Germany, Paolo G. Giarrusso University of Tübingen, Germany, Klaus Ostermann University of Tübingen, Germany Media Attached | ||
11:45 25mTalk | A Theory of Effects and Resources: Adjunction Models and Polarised Calculi Research Papers Pierre-Louis Curien Univ. Paris Diderot and INRIA Paris-Rocquencourt, Marcelo Fiore Computer Laboratory, University of Cambridge, Guillaume Munch-Maccagnoni Computer Laboratory, University of Cambridge | ||