Simon Huber
Postdoc in the
Programming Logic Group at the
Department of Computer Science and Engineering,
University of Gothenburg.
Publications and drafts
- 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.
Some slides from talks
- Homotopy canonicity for
cubical type theory, 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.
Other
Current teaching
Contact
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