new slides |
v v |
9/23/16 |

CoqPL 2017: Call for Presentations for the Workshop on Coq for Programming Languages |
Emilio Jesús Gallego Arias |
9/22/16 |

Semantic Success Condition for the definability of Semi-Simplicial Types |
Dimitris Tsementzis |
9/21/16 |

A puzzle about "univalent equality" |
Andrew Polonsky |
9/19/16 |

In case you haven’t heard what’s going on in Leicester … |
Martin Hotzel Escardo |
9/16/16 |

weak univalence with "beta" implies full univalence |
Dan Licata |
9/15/16 |

Postdoctoral position in univalent foundations and type theory at the IAS |
v v |
9/12/16 |

Meta-conjecture about MLTT |
Martin Hotzel Escardo |
9/12/16 |

Workshop on Categorical Logic and Univalent Foundations: slides available |
Christian Sattler |
8/15/16 |

Cubical sets and the topological topos |
Bas Spitters |
8/8/16 |

Fwd: Fellowship Opportunity for < 5 yrs from PhD - Power of Information |
v v |
8/7/16 |

post-doc at Wesleyan |
Dan Licata |
8/5/16 |

ICMS 2016 most special session slides added |
v v |
7/28/16 |

FOMUS slides |
v v |
7/26/16 |

CFP: special issue of JAR on HoTT and univalent foundations |
nicolas tabareau |
7/25/16 |

What's so great about decidable proof checking? |
Matt Oliveri |
7/20/16 |

Different notions of equality; terminology |
Andrew Polonsky |
7/19/16 |

Fwd: [PVS] tenure track position in Theoretical Computer Science |
v v |
7/8/16 |

Guarded Cubical Type Theory |
Bas Spitters |
6/24/16 |

PhD thesis: On the homotopy groups of spheres in homotopy type theory |
Guillaume Brunerie |
6/21/16 |