| Publication | Date of Publication | Type |
|---|
| A metatheoretic analysis of subtype universes | 2024-11-26 | Paper |
| Propositional forms of judgemental interpretations | 2023-10-24 | Paper |
| Gradability in MTT-Semantics | 2022-08-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4964710 | 2021-03-03 | Paper |
| Adjectival and adverbial modification: the view from modern type theories | 2018-02-08 | Paper |
| Dependent event types | 2017-12-20 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4599196 | 2017-12-18 | Paper |
| Proof Assistants for Natural Language Semantics | 2017-02-22 | Paper |
| Weyl's predicative classical mathematics as a logic-enriched type theory | 2015-09-17 | Paper |
| Natural language inference in Coq | 2015-02-27 | Paper |
| Common Nouns as Types | 2014-06-24 | Paper |
| Formal Semantics in Modern Type Theories: Is It Model-Theoretic, Proof-Theoretic, or Both? | 2014-06-24 | Paper |
| Dot-types and Their Implementation | 2014-06-24 | Paper |
| Monotonicity Reasoning in Formal Semantics Based on Modern Type Theories | 2014-06-24 | Paper |
| Coercive subtyping: theory and implementation | 2013-06-06 | Paper |
| A pluralist approach to the formalisation of mathematics | 2011-10-21 | Paper |
| Classical predicative logic-enriched type theories | 2011-08-26 | Paper |
| Contextual Analysis of Word Meanings in Type-Theoretical Semantics | 2011-07-01 | Paper |
| Coherence and Transitivity in Coercive Subtyping | 2011-05-06 | Paper |
| Manifest Fields and Module Mechanisms in Intensional Type Theory | 2009-07-02 | Paper |
| Weyl’s Predicative Classical Mathematics as a Logic-Enriched Type Theory | 2009-03-10 | Paper |
| Structural subtyping for inductive types with functorial equality rules | 2008-11-13 | Paper |
| Coercions in a polymorphic type system | 2008-08-15 | Paper |
| Types for Proofs and Programs | 2005-12-23 | Paper |
| Types for Proofs and Programs | 2005-12-23 | Paper |
| Transitivity in coercive subtyping | 2005-05-12 | Paper |
| PAL+: a lambda-free logical framework | 2004-03-17 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4435472 | 2003-11-12 | Paper |
| An implementation of LF with coercive subtyping and universes | 2003-11-05 | Paper |
| Coercion completion and conservativity in coercive subtyping | 2003-05-29 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2766802 | 2002-07-08 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2757819 | 2001-12-04 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2736340 | 2001-08-29 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4499226 | 2001-03-04 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4263084 | 2000-04-25 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4246948 | 1999-12-13 | Paper |
| Coercive subtyping | 1999-03-30 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4362923 | 1997-11-13 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4296744 | 1994-06-20 | Paper |
| Program specification and data refinement in type theory | 1994-03-14 | Paper |
| A higher-order calculus and theory abstraction | 1991-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3211296 | 1989-01-01 | Paper |
