All Outputs (10)

Two-level type theory and applications (2023)
Journal Article
Annenkov, D., Capriotti, P., Kraus, N., & Sattler, C. (2023). Two-level type theory and applications. Mathematical Structures in Computer Science, 33(8), 688-743. https://doi.org/10.1017/s0960129523000130

We define and develop two-level type theory (2LTT), a version of Martin-Löf type theory which combines two different type theories. We refer to them as the ‘inner’ and the ‘outer’ type theory. In our case of interest, the inner theory is homotopy typ... Read More about Two-level type theory and applications.

Type-theoretic approaches to ordinals (2023)
Journal Article
Kraus, N., Nordvall Forsberg, F., & Xu, C. (2023). Type-theoretic approaches to ordinals. Theoretical Computer Science, 957, Article 113843. https://doi.org/10.1016/j.tcs.2023.113843

In a constructive setting, no concrete formulation of ordinal numbers can simultaneously have all the properties one might be interested in; for example, being able to calculate limits of sequences is constructively incompatible with deciding extensi... Read More about Type-theoretic approaches to ordinals.

A rewriting coherence theorem with applications in homotopy type theory (2022)
Journal Article
Kraus, N., & von Raumer, J. (2022). A rewriting coherence theorem with applications in homotopy type theory. Mathematical Structures in Computer Science, 32(7), 982-1014. https://doi.org/10.1017/s0960129523000026

Higher-dimensional rewriting systems are tools to analyse the structure of formally reducing terms to normal forms, as well as comparing the different reduction paths that lead to those normal forms. This higher structure can be captured by finding a... Read More about A rewriting coherence theorem with applications in homotopy type theory.

Shallow Embedding of Type Theory is Morally Correct (2019)
Journal Article
Kaposi, A., Kovács, A., & Kraus, N. (2019). Shallow Embedding of Type Theory is Morally Correct. Lecture Notes in Artificial Intelligence, 11825 LNCS, 329-365. https://doi.org/10.1007/978-3-030-33636-3_12

© 2019, Springer Nature Switzerland AG. There are multiple ways to formalise the metatheory of type theory. For some purposes, it is enough to consider specific models of a type theory, but sometimes it is necessary to refer to the syntax, for exampl... Read More about Shallow Embedding of Type Theory is Morally Correct.

Univalent higher categories via complete semi-segal types (2017)
Journal Article
Capriotti, P., & Kraus, N. (2018). Univalent higher categories via complete semi-segal types. Proceedings of the ACM on Programming Languages, 2(POPL), https://doi.org/10.1145/3158132

Category theory in homotopy type theory is intricate as categorical laws can only be stated “up to homotopy”, and thus require coherences. The established notion of a univalent category (as introduced by Ahrens et al.)solves this by considering only... Read More about Univalent higher categories via complete semi-segal types.

Notions of anonymous existence in Martin-Löf type theory (2017)
Journal Article
Kraus, N., Escardo, M., Coquand, T., & Altenkirch, T. (in press). Notions of anonymous existence in Martin-Löf type theory. Logical Methods in Computer Science, 13(1),

As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-L\"of type theory cannot generally be shown to be unique. Inspired by a theorem by Hedberg, we give some simple characterizations of types that do have uniqu... Read More about Notions of anonymous existence in Martin-Löf type theory.

The General Universal Property of the Propositional Truncation (2015)
Journal Article
Kraus, N. (2015). The General Universal Property of the Propositional Truncation. LIPIcs, 39, 111-145. https://doi.org/10.4230/LIPIcs.TYPES.2014.111

In a type-theoretic fibration category in the sense of Shulman (representing a dependent type theory with at least 1, Sigma, Pi, and identity types), we define the type of constant functions from A to B. This involves an infinite tower of coherence c... Read More about The General Universal Property of the Propositional Truncation.

Functions out of Higher Truncations (2015)
Journal Article
Capriotti, P., Kraus, N., & Vezzosi, A. (2015). Functions out of Higher Truncations. LIPIcs, 41, https://doi.org/10.4230/LIPIcs.CSL.2015.359

In homotopy type theory, the truncation operator ||-||n (for a number n > -2) is often useful if one does not care about the higher structure of a type and wants to avoid coherence problems. However, its elimination principle only allows to eliminate... Read More about Functions out of Higher Truncations.

Higher Homotopies in a Hierarchy of Univalent Universes (2015)
Journal Article
Kraus, N., & Sattler, C. (2015). Higher Homotopies in a Hierarchy of Univalent Universes. ACM Transactions on Computational Logic, 16(2), https://doi.org/10.1145/2729979

For Martin-Lof type theory with a hierarchy U(0): U(1): U(2): ... of univalent universes, we show that U(n) is not an n-type. Our construction also solves the problem of finding a type that strictly has some high truncation level without using higher... Read More about Higher Homotopies in a Hierarchy of Univalent Universes.

A Lambda Term Representation Inspired by Linear Ordered Logic (2011)
Journal Article
Abel, A., & Kraus, N. (2011). A Lambda Term Representation Inspired by Linear Ordered Logic. Electronic Proceedings in Theoretical Computer Science, 71, 1-13. https://doi.org/10.4204/EPTCS.71.1

We introduce a new nameless representation of lambda terms inspired by ordered logic. At a lambda abstraction, number and relative position of all occurrences of the bound variable are stored, and application carries the additional information where... Read More about A Lambda Term Representation Inspired by Linear Ordered Logic.