Simon Huber
Postdoc in the
Programming Logic Group at the
Department of Computer Science and Engineering,
University of Gothenburg.
Publications and drafts
- The univalence axiom in cubical
sets (with Marc Bezem and Thierry Coquand), preprint,
2016.
- Canonicity for
Cubical Type Theory, preprint, 2016.
- Cubical Type Theory: a
constructive interpretation of the univalence axiom
[arXiv] (with
Cyril Cohen, Thierry Coquand, and Anders Mörtberg), to appear in
the proceedings of TYPES 2015, 2015.
- 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.
Some slides from talks
- 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.
Other
Contact
Email: simon.huber(at)cse(dot)gu(dot)se
or simonhu(at)chalmers(dot)se
Tel: +46 (31) 772 54 10 (defunct)
Rännvägen 6
Rum 6103, floor 6
EDIT building, Campus Johanneberg