| Publication | Date of Publication | Type |
|---|
| A formal description of an algorithm suitable for parsing the language of mathematics | 2026-02-19 | Paper |
| Intersection types via finite-set declarations | 2025-01-31 | Paper |
| Towards semantic markup of mathematical documents via user interaction | 2024-12-04 | Paper |
Isabelle/HOL/GST: a formal proof environment for generalized set theories
Lecture Notes in Computer Science | 2023-06-02 | Paper |
| Generating custom set theories with non-set structured objects | 2022-04-22 | Paper |
Adding an abstraction barrier to ZF set theory
(available as arXiv preprint) | 2021-01-20 | Paper |
| BNF-style notation as it is actually used | 2020-01-22 | Paper |
| scientific article; zbMATH DE number 7015116 (Why is no real title available?) | 2019-02-07 | Paper |
Strongly typed flow-directed representation transformations (extended abstract)
Proceedings of the second ACM SIGPLAN international conference on Functional programming | 2017-08-21 | Paper |
Skalpel: a constraint-based type error slicer for standard ML
Journal of Symbolic Computation | 2017-02-06 | Paper |
Bridging Curry and Church's typing style
Journal of Applied Logic | 2016-10-31 | Paper |
Automath type inclusion in Barendregt's cube
Lecture Notes in Computer Science | 2015-10-20 | Paper |
Functioning without closure: type-safe customized function representations for standard ML
Proceedings of the sixth ACM SIGPLAN international conference on Functional programming | 2015-03-09 | Paper |
Type inference, principal typings, and let-polymorphism for first-class mixin modules
Proceedings of the tenth ACM SIGPLAN international conference on Functional programming | 2015-01-06 | Paper |
Computerizing mathematical text with MathLang
Electronic Notes in Theoretical Computer Science | 2013-12-13 | Paper |
| Expansion: the crucial mechanism for type inference with intersection types: a survey and explanation | 2013-10-02 | Paper |
| MathLang: experience-driven development of a new mathematical language | 2013-09-09 | Paper |
Implementing compositional analysis using intersection types with expansion variables
Electronic Notes in Theoretical Computer Science | 2013-08-16 | Paper |
On realisability semantics for intersection types with expansion variables
Fundamenta Informaticae | 2013-01-24 | Paper |
Reducibility Proofs in the λ-Calculus
Fundamenta Informaticae | 2013-01-24 | Paper |
The algebra of expansion
Fundamenta Informaticae | 2013-01-24 | Paper |
Expansion for universal quantifiers
Programming Languages and Systems | 2012-06-22 | Paper |
Compilation of extended recursion in call-by-value functional languages
Higher-Order and Symbolic Computation | 2010-03-05 | Paper |
MathLang Translation to Isabelle Syntax
Lecture Notes in Computer Science | 2009-07-09 | Paper |
| Realisability Semantics for Intersection Types and Expansion Variables | 2009-05-13 | Paper |
A Complete Realisability Semantics for Intersection Types and Arbitrary Expansion Variables
Theoretical Aspects of Computing - ICTAC 2008 | 2009-01-27 | Paper |
Graph-Based Proof Counting and Enumeration with Applications for Program Fragment Synthesis
Logic Based Program Synthesis and Transformation | 2008-04-24 | Paper |
Restoring Natural Language as a Computerised Mathematics Input Method
Towards Mechanized Mathematical Assistants | 2007-11-28 | Paper |
Narrative Structure of Mathematical Texts
Towards Mechanized Mathematical Assistants | 2007-11-28 | Paper |
Programming Languages and Systems
Lecture Notes in Computer Science | 2007-09-28 | Paper |
Programming Languages and Systems
Lecture Notes in Computer Science | 2007-09-28 | Paper |
Mathematical Knowledge Management
Lecture Notes in Computer Science | 2007-02-12 | Paper |
Programming Languages and Systems
Lecture Notes in Computer Science | 2005-09-13 | Paper |
Mathematical Knowledge Management
Lecture Notes in Computer Science | 2005-08-26 | Paper |
| scientific article; zbMATH DE number 2163048 (Why is no real title available?) | 2005-04-29 | Paper |
Type error slicing in implicitly typed higher-order languages
Science of Computer Programming | 2004-11-22 | Paper |
Principality and type inference for intersection types using expansion variables
Theoretical Computer Science | 2004-10-27 | Paper |
| scientific article; zbMATH DE number 2086682 (Why is no real title available?) | 2004-08-11 | Paper |
| scientific article; zbMATH DE number 2087541 (Why is no real title available?) | 2004-08-11 | Paper |
| scientific article; zbMATH DE number 2043523 (Why is no real title available?) | 2004-02-16 | Paper |
| scientific article; zbMATH DE number 1956560 (Why is no real title available?) | 2003-07-30 | Paper |
A calculus with polymorphic and polyvariant flow types
Journal of Functional Programming | 2002-10-06 | Paper |
| scientific article; zbMATH DE number 1746456 (Why is no real title available?) | 2002-05-28 | Paper |
| scientific article; zbMATH DE number 1538035 (Why is no real title available?) | 2001-05-20 | Paper |
Cut rules and explicit substitutions
MSCS. Mathematical Structures in Computer Science | 2001-05-07 | Paper |
Typability and type checking in System F are equivalent and undecidable
Annals of Pure and Applied Logic | 1999-09-22 | Paper |
| scientific article; zbMATH DE number 1332643 (Why is no real title available?) | 1999-09-09 | Paper |
Intersection Types via Finite-Set Declarations
(available as arXiv preprint) | N/A | Paper |
