Postdoc in the Programming Logic Group at the Department of Computer Science and Engineering, University of Gothenburg.

- Homotopy canonicity for cubical type theory (with Thierry Coquand and Christian Sattler), preprint, 2019.
- Gluing for type theory (with Ambrus Kaposi and Christian Sattler), preprint, 2019.
- On Higher Inductive Types in Cubical Type Theory [journal, arXiv] (with Thierry Coquand and Anders Mörtberg), Proceedings of LICS 2018, 2018.
- An Adequacy Theorem for Dependent Type Theory [journal] (with Thierry Coquand), Theory of Computing Systems, 2018.
- The univalence axiom in cubical sets [journal, arXiv] (with Marc Bezem and Thierry Coquand), Journal of Automated Reasoning, 2018.
- Canonicity for Cubical Type Theory [journal, arXiv], Journal of Automated Reasoning, 2018.
- Cubical Type Theory: a constructive interpretation of the univalence axiom [journal, arXiv] (with Cyril Cohen, Thierry Coquand, and Anders Mörtberg), Proceedings of TYPES 2015, 2018.
- A Model of Type Theory in Cubical Sets [journal] (with Marc Bezem and Thierry Coquand), Proceedings of TYPES 2013, 2014.
- A generalization of the Takeuti–Gandy interpretation [journal] (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.

- 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.

- A note about a variant of cubical type theory suited for higher inductive types, 2017.
- Cubical Intepretations of Type Theory [GUPEA], PhD Thesis, 2016.
- A Model of Type Theory in Cubical Sets, Licentiate Thesis, 2015.
- cubical and cubicaltt: proof assistants based on the cubical set models.
- On the Computational Content of Choice Axioms, Diploma Thesis, 2010.

- Logic in Computer Science (DAT060/DIT201), LP1 2018/2019.

Email: `simon.huber(at)cse(dot)gu(dot)se`

or `simonhu(at)chalmers(dot)se`

Tel: +46733052426, +46 (31) 772 69 33

Rännvägen 6

Rum 6103, floor 6

EDIT building, Campus Johanneberg