Write a Blog >>
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 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

10:30 - 12:10
Track 2: Types and FoundationsResearch Papers at Grand Bay South
Chair(s): Robert AtkeyUniversity of Strathclyde
10:30
25m
Talk
Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega
Research Papers
Matt BrownUCLA, Jens PalsbergUniversity of California, Los Angeles
Media Attached File Attached
10:55
25m
Talk
Type Theory in Type Theory using Quotient Inductive Types
Research Papers
Thorsten AltenkirchUniversity of Nottingham, Ambrus KaposiUniversity of Nottingham
Media Attached File Attached
11:20
25m
Talk
System Fω with Equirecursive Types for Datatype-generic Programming
Research Papers
Yufei CaiUniversity of Tübingen, Germany, Paolo G. GiarrussoUniversity of Tübingen, Germany, Klaus OstermannUniversity of Tübingen, Germany
Media Attached
11:45
25m
Talk
A Theory of Effects and Resources: Adjunction Models and Polarised Calculi
Research Papers
Pierre-Louis CurienUniv. Paris Diderot and INRIA Paris-Rocquencourt, Marcelo FioreComputer Laboratory, University of Cambridge, Guillaume Munch-MaccagnoniComputer Laboratory, University of Cambridge