CPP 2016
Mon 18 - Tue 19 January 2016 St. Petersburg, Florida, United States
co-located with POPL 2016
Tue 19 Jan 2016 11:00 - 11:30 at Room St Petersburg II - Session 6: Foundations

In homotopy type theory, we construct the propositional truncation as a colimit, using only non-recursive higher inductive types (HITs). This is a first step towards reducing recursive HITs to non-recursive HITs. This construction gives a characterization of functions from the propositional truncation to an arbitrary type, extending the universal property of the propositional truncation. We have fully formalized all results in a new proof assistant, Lean.

I am currently a third year Ph.D. student in the Philosophy Department at Carnegie Mellon University. My advisor is Jeremy Avigad and I am also working together with Steve Awodey. I am enrolled in the Pure and Applied Logic program.

I previously studied at the Utrecht University in the Netherlands where I received a B.Sc. in Mathematics, a B.Sc. in Physics and a M.Sc. in Mathematics. My master thesis is Explicit convertibility proofs in Pure Type Systems supervised by Freek Wiedijk at the Radboud University Nijmegen. I was also trainer for the Dutch Mathematical Olympiad.

Tue 19 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

10:30 - 12:00
Session 6: FoundationsCPP at Room St Petersburg II
10:30
30m
Talk
A Logic of Proofs for Differential Dynamic Logic
CPP
Nathan Fulton Carnegie Mellon University, André Platzer
11:00
30m
Talk
Constructing the Propositional Truncation using Non-recursive HITs
CPP
Floris van Doorn Carnegie Mellon University
11:30
30m
Talk
A Nominal Exploration of Intuitionism
CPP
Vincent Rahli SnT, Mark Bickford Cornell University