Homotopy Type Theory and Computing – Classical and Quantum


WHEN April 19-21, 2024
WHERE NYU Abu Dhabi WHO NYUAD Center for Quantum and Topological Systems By Invitation Interested scholars please contact nyuad.cqts.info@nyu.edu

The aim of this conference is to discuss Homotopy Type Theory Theory (HoTT) as a substrate for computing and verification in software development, in synthetic homotopy theory, and possibly in application to (topological) quantum computing/simulation.

Some talks will focus on recent progress on the general issue of running HoTT programs, in view of the univalence axiom: such as via “cubical TT” or the more recent “higher observational TT.” Other talks will focus on design patterns for practical (quantum) programming and certification languages, notably via modal types and monadic effects (in modal extensions of HoTT).

In this vein, our local speakers will present a point of contact between modal HoTT and Quantum: the recently developed “Linear HoTT” (LHoTT) that equips classical HoTT with dependent “linear” types which may be thought of as quantum data types. The LHoTT approach to quantum programming interprets a significant fragment of the Proto-Quipper-language, now with identity types enabling full verification.

The conference brings this theoretical progress into contact with efforts to use (L)HoTT and related languages like Proto-Quipper for actual (quantum) computing, simulation, and verification.

  • Speakers and Abstracts

Join our events mailing lists

Always be the first to know about what's going on in our community. Sign up for one of our newsletters and receive information on a wide variety of events such as exhibition, lectures, films, art performances, discussions and conferences.

Join The Arts Center events mailing list Join The Institute events mailing list Join The Art Gallery events mailing list Join The StartAD events mailing list