| Publication | Date of Publication | Type |
|---|
| A metatheoretic analysis of subtype universes | 2024-11-26 | Paper |
Propositional forms of judgemental interpretations
Journal of Logic, Language and Information | 2023-10-24 | Paper |
| Gradability in MTT-Semantics | 2022-08-11 | Paper |
| Typed operational semantics for dependent record types | 2021-03-03 | Paper |
Typed operational semantics for dependent record types
(available as arXiv preprint) | 2021-03-03 | Paper |
Adjectival and adverbial modification: the view from modern type theories
Journal of Logic, Language and Information | 2018-02-08 | Paper |
| Dependent event types | 2017-12-20 | Paper |
| Individuation criteria, dot-types and copredication: a view from modern type theories | 2017-12-18 | Paper |
Proof assistants for natural language semantics
Logical Aspects of Computational Linguistics. Celebrating 20 Years of LACL (1996–2016) | 2017-02-22 | Paper |
Weyl's predicative classical mathematics as a logic-enriched type theory
ACM Transactions on Computational Logic | 2015-09-17 | Paper |
Natural language inference in Coq
Journal of Logic, Language and Information | 2015-02-27 | Paper |
Common nouns as types
Logical Aspects of Computational Linguistics | 2014-06-24 | Paper |
Formal semantics in modern type theories: is it model-theoretic, proof-theoretic, or both?
Logical Aspects of Computational Linguistics | 2014-06-24 | Paper |
Dot-types and their implementation
Logical Aspects of Computational Linguistics | 2014-06-24 | Paper |
Monotonicity reasoning in formal semantics based on modern type theories
Logical Aspects of Computational Linguistics | 2014-06-24 | Paper |
Coercive subtyping: theory and implementation
Information and Computation | 2013-06-06 | Paper |
A pluralist approach to the formalisation of mathematics
Mathematical Structures in Computer Science | 2011-10-21 | Paper |
Classical predicative logic-enriched type theories
Annals of Pure and Applied Logic | 2011-08-26 | Paper |
Classical predicative logic-enriched type theories
Annals of Pure and Applied Logic | 2011-08-26 | Paper |
Contextual analysis of word meanings in type-theoretical semantics
Logical Aspects of Computational Linguistics | 2011-07-01 | Paper |
Coherence and Transitivity in Coercive Subtyping
Logic for Programming, Artificial Intelligence, and Reasoning | 2011-05-06 | Paper |
Manifest Fields and Module Mechanisms in Intensional Type Theory
Lecture Notes in Computer Science | 2009-07-02 | Paper |
Weyl’s Predicative Classical Mathematics as a Logic-Enriched Type Theory
Lecture Notes in Computer Science | 2009-03-10 | Paper |
Structural subtyping for inductive types with functorial equality rules
Mathematical Structures in Computer Science | 2008-11-13 | Paper |
Coercions in a polymorphic type system
Mathematical Structures in Computer Science | 2008-08-15 | Paper |
Types for Proofs and Programs
Lecture Notes in Computer Science | 2005-12-23 | Paper |
Types for Proofs and Programs
Lecture Notes in Computer Science | 2005-12-23 | Paper |
Transitivity in coercive subtyping
Information and Computation | 2005-05-12 | Paper |
PAL+: a lambda-free logical framework
Journal of Functional Programming | 2004-03-17 | Paper |
| scientific article; zbMATH DE number 2003159 (Why is no real title available?) | 2003-11-12 | Paper |
An implementation of LF with coercive subtyping and universes
Journal of Automated Reasoning | 2003-11-05 | Paper |
Coercion completion and conservativity in coercive subtyping
Annals of Pure and Applied Logic | 2003-05-29 | Paper |
| scientific article; zbMATH DE number 1696611 (Why is no real title available?) | 2002-07-08 | Paper |
| scientific article; zbMATH DE number 1678369 (Why is no real title available?) | 2001-12-04 | Paper |
| scientific article; zbMATH DE number 1638644 (Why is no real title available?) | 2001-08-29 | Paper |
| scientific article; zbMATH DE number 1497808 (Why is no real title available?) | 2001-03-04 | Paper |
| scientific article; zbMATH DE number 1341542 (Why is no real title available?) | 2000-04-25 | Paper |
| scientific article; zbMATH DE number 1301735 (Why is no real title available?) | 1999-12-13 | Paper |
Coercive subtyping
Journal Of Logic And Computation | 1999-03-30 | Paper |
| scientific article; zbMATH DE number 1086673 (Why is no real title available?) | 1997-11-13 | Paper |
| scientific article; zbMATH DE number 591911 (Why is no real title available?) | 1994-06-20 | Paper |
Program specification and data refinement in type theory
Mathematical Structures in Computer Science | 1994-03-14 | Paper |
A higher-order calculus and theory abstraction
Information and Computation | 1991-01-01 | Paper |
| scientific article; zbMATH DE number 4191621 (Why is no real title available?) | 1989-01-01 | Paper |
