Simon Huber

This page collects some of my academic output. I was a postdoc in the Programming Logic Group at the Department of Computer Science and Engineering, University of Gothenburg. Prior to that I wrote my PhD thesis under supervision of Thierry Coquand also at the University of Gothenburg.

Publications and drafts

• Canonicity and homotopy canonicity for cubical type theory [doi, arXiv] (with Thierry Coquand and Christian Sattler), Logical Methods in Computer Science, Volume 18, Issue 1, 2022.
• Homotopy canonicity for cubical type theory [doi] (with Thierry Coquand and Christian Sattler), Proceedings of FSCD 2019, 2019.
• Gluing for type theory [doi] (with Ambrus Kaposi and Christian Sattler), Proceedings of FSCD 2019, 2019.
• On Higher Inductive Types in Cubical Type Theory [doi, arXiv] (with Thierry Coquand and Anders Mörtberg), Proceedings of LICS 2018, 2018.
• An Adequacy Theorem for Dependent Type Theory [doi] (with Thierry Coquand), Theory of Computing Systems, 2018.
• The univalence axiom in cubical sets [doi, arXiv] (with Marc Bezem and Thierry Coquand), Journal of Automated Reasoning, 2018.
• Canonicity for Cubical Type Theory [doi, arXiv], Journal of Automated Reasoning, 2018.
• Cubical Type Theory: a constructive interpretation of the univalence axiom [doi, arXiv] (with Cyril Cohen, Thierry Coquand, and Anders Mörtberg), Proceedings of TYPES 2015, 2018.
• A Model of Type Theory in Cubical Sets [doi] (with Marc Bezem and Thierry Coquand), Proceedings of TYPES 2013, 2014.
• A generalization of the Takeuti–Gandy interpretation [doi] (with Bruno Barras and Thierry Coquand), Mathematical Structures of Computer Science, Volume 25, Special Issue 05, pp. 1071-1099, 2015.
• Towards a formal theory of computability (with Helmut Schwichtenberg and Basil Karádais), In: R. Schindler, ed., Ways of Proof Theory: Festschrift for W. Pohlers, 2010.

Some slides from talks

• Homotopy canonicity for cubical type theory [video], HoTT Electronic Seminar Talks, February 2019.
• Lectures on Homotopy Type Theory (1, 2), Summer School on Types, Sets and Constructions, Hausdorff Research Institute for Mathematics, Bonn, May 2018.
• Canonicity for Cubical Type Theory, EUTypes meeting, Ljubljana, 31 January 2017.
• Cubical Intepretations of Type Theory, PhD defense, Gothenburg, 29 November 2016.
• A Cubical Type Theory, DMV Jahrestagung 2015, Hamburg, 25 September 2015.
• A Cubical Type Theory, HoTT/UF 2015, Warsaw, 29 June 2015.
• Implementing a Variation of the Cubical Set Model, ProgLog Seminar, November 2014.
• A Model of Type Theory in Cubical Sets, Constructive Mathematics and Models of Type Theory, IHP, Paris, 5 June 2014.
• A Model of Type Theory in Cubical Sets, Conference on Type Theory, Homotopy Theory and Univalent Foundations, Barcelona, 23 September 2013.
• Constructive Kan Fibrations, HDACT 2012, Ljubljana, 20 June 2012.
• Towards a Computational Justification of the Univalence Axiom, TYPES 2011, Bergen, 11 September 2011.

Theses

• Cubical Intepretations of Type Theory [GUPEA], PhD Thesis, 2016.
• A Model of Type Theory in Cubical Sets, Licentiate Thesis, 2015.
• On the Computational Content of Choice Axioms, Diploma Thesis, 2010.

Other

• An unfinished attempt to define an initial E-cwf with a total interpretation function in Agda.
• A note about a variant of cubical type theory suited for higher inductive types, 2017.
• cubical and cubicaltt: proof assistants based on the cubical set models.

Contact

Email: simonh@fripost.org