Category Archives: Programming

A Formalized Interpreter

I’d like to announce a result that might be interesting: an interpreter for a very small dependent type system in Coq, assuming uniqueness of identity proofs (UIP). Because it assumes UIP, it’s not immediately compatible with HoTT, but it seems … Continue reading

Posted in Code, Foundations, Programming | 77 Comments

Abstract Types with Isomorphic Types

Here’s a cute little example of programming in HoTT that I worked out for a recent talk. Abstract Types One of the main ideas used to structure large programs is abstract types. You give a specification for a component, and … Continue reading

Posted in Programming, Uncategorized | 8 Comments

Canonicity for 2-Dimensional Type Theory

A consequence of the univalence axiom is that isomorphic types are equivalent (propositionally equal), and therefore interchangable in any context (by the identity eliminaiton rule J). Type isomorphisms arise frequently in dependently typed programming, where types are often refined to … Continue reading

Posted in Foundations, Programming, Univalence | 8 Comments