Thorsten Altenkirch, Paolo Capriotti & Nicolai Kraus (2016):
Extending Homotopy Type Theory with Strict Equality,
doi:10.4230/LIPIcs.CSL.2016.21.
Carlo Angiuli, Kuen-Bang Hou (Favonia) & Robert Harper (2018):
Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities.
In: Dan R. Ghica & Achim Jung: 27th EACSL Annual Conference on Computer Science Logic, CSL 2018, September 4-7, 2018, Birmingham, UK,
LIPIcs 119.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
pp. 6:1–6:17,
doi:10.4230/LIPIcs.CSL.2018.6.
Danil Annenkov, Paolo Capriotti, Nicolai Kraus & Christian Sattler (2017):
Two-Level Type Theory and Applications.
Ali Assaf (2015):
Conservativity of Embeddings in the lambda Pi Calculus Modulo Rewriting.
In: Thorsten Altenkirch: 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015, July 1-3, 2015, Warsaw, Poland,
LIPIcs 38.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
pp. 31–44,
doi:10.4230/LIPIcs.TLCA.2015.31.
Ali Assaf, Guillaume Burel, Raphaël Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant & Ronan Saillard (2016):
Dedukti: a logical framework based on the λΠ-calculus modulo theory.
Unpublished manuscript.
Available at http://www.lsv.fr/~dowek/Publi/expressing.pdf.
Bruno Barras, Jean-Pierre Jouannaud, Pierre-Yves Strub & Qian Wang (2011):
CoQMTU: A Higher-Order Type Theory with a Predicative Hierarchy of Universes Parametrized by a Decidable First-Order Theory.
In: Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, June 21-24, 2011, Toronto, Ontario, Canada.
IEEE Computer Society,
pp. 143–151,
doi:10.1109/LICS.2011.37.
Cyril Cohen, Thierry Coquand, Simon Huber & Anders Mörtberg (2016):
Cubical Type Theory: a constructive interpretation of the univalence axiom.
Martin Hofmann (1997):
Syntax and semantics of dependent types.
The Univalent Foundations Program (2013):
Homotopy Type Theory: Univalent Foundations of Mathematics.
https://homotopytypetheory.org/book,
Institute for Advanced Study.
Théo Winterhalter, Matthieu Sozeau & Nicolas Tabareau (2019):
Eliminating reflection from type theory.
In: Assia Mahboubi & Magnus O. Myreen: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019.
ACM,
pp. 91–103,
doi:10.1145/3293880.3294095.
eptcs@eptcs.org