| Publication | Date of Publication | Type |
|---|
| A formal description of an algorithm suitable for parsing the language of mathematics | 2026-02-19 | Paper |
| Towards semantic markup of mathematical documents via user interaction | 2024-12-04 | Paper |
| Introduction | 2024-09-06 | Paper |
| Substitution in the \(\lambda\)-calculus and the role of the Curry school | 2024-09-06 | Paper |
| A primer of mathematical analysis and the foundations of computation | 2024-03-01 | Paper |
Thoughts on Using the History of Mathematics to Teach the Foundations of Mathematical Analysis
Annals of the Canadian Society for History and Philosophy of Mathematics/ Société canadienne d’histoire et de philosophie des mathématiques | 2023-06-14 | 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 |
Explicit substitution calculi with de Bruijn indices and intersection type systems
Logic Journal of the IGPL | 2019-01-08 | 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 |
The soundness of explicit substitution with nameless variables
International Journal of Foundations of Computer Science | 2015-04-29 | Paper |
Simplified reducibility proofs of Church-Rosser for \({\beta}\)- and \({\beta}{\eta}\)-reduction
Electronic Notes in Theoretical Computer Science | 2015-03-18 | Paper |
A flexible framework for visualisation of computational properties of general explicit substitutions calculi
Electronic Notes in Theoretical Computer Science | 2015-03-18 | Paper |
Computerizing mathematical text with MathLang
Electronic Notes in Theoretical Computer Science | 2013-12-13 | Paper |
| MathLang: experience-driven development of a new mathematical language | 2013-09-09 | Paper |
Automath and Pure Type Systems
Electronic Notes in Theoretical Computer Science | 2013-06-06 | Paper |
Explicit substitutions à la de Bruijn: the local and global way
Electronic Notes in Theoretical Computer Science | 2013-06-06 | Paper |
Comparing calculi of explicit substitutions with eta-reduction
Electronic Notes in Theoretical Computer Science | 2013-04-19 | Paper |
On automating the extraction of programs from proofs using product types
Electronic Notes in Theoretical Computer Science | 2013-04-19 | 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 |
Russell's Orders in Kripke's Theory of Truth and Computational Type Theory
Handbook of the History of Logic | 2012-10-12 | Paper |
On functions and types: a tutorial
SOFSEM 2002: Theory and Practice of Informatics | 2011-04-01 | Paper |
| Intersection type system with de Bruijn indices | 2011-03-30 | Paper |
Intersection type systems and explicit substitutions calculi
Logic, Language, Information and Computation | 2010-09-29 | Paper |
Explicit substitutions calculi with one step eta-reduction decided explicitly
Logic Journal of the IGPL | 2009-12-18 | Paper |
SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi
Journal of Applied Non-Classical Logics | 2009-11-30 | 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 |
Principal Typings for Explicit Substitutions Calculi
Logic and Theory of Algorithms | 2008-06-19 | Paper |
Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions
Journal of Applied Logic | 2008-04-07 | Paper |
The Weak Normalization of the Simply Typed se-calculus
Logic Journal of the IGPL | 2008-01-14 | 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 |
A completeness result for a realisability semantics for an intersection type system
Annals of Pure and Applied Logic | 2007-05-23 | Paper |
Mathematical Knowledge Management
Lecture Notes in Computer Science | 2007-02-12 | Paper |
| Logical reasoning. A first course | 2006-03-27 | Paper |
Logic for Programming, Artificial Intelligence, and Reasoning
Lecture Notes in Computer Science | 2005-11-10 | Paper |
Typed $\lambda$-calculi with one binder
Journal of Functional Programming | 2005-10-11 | Paper |
| scientific article; zbMATH DE number 2208065 (Why is no real title available?) | 2005-09-26 | Paper |
Mathematical Knowledge Management
Lecture Notes in Computer Science | 2005-08-26 | Paper |
AN EXTENSION OF AN AUTOMATED TERMINATION METHOD OF RECURSIVE FUNCTIONS
International Journal of Foundations of Computer Science | 2005-06-22 | Paper |
Comparing and implementing calculi of explicit substitutions with eta-reduction
Annals of Pure and Applied Logic | 2005-06-01 | Paper |
| scientific article; zbMATH DE number 2154395 (Why is no real title available?) | 2005-04-09 | Paper |
De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: The typed case
The Journal of Logic and Algebraic Programming | 2005-02-22 | Paper |
De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: the untyped case
The Journal of Logic and Algebraic Programming | 2005-02-22 | Paper |
A modern perspective on type theory. From its origins until today
Applied Logic Series | 2004-11-25 | Paper |
A refinement of de Bruijn's formal language of mathematics
Journal of Logic, Language and Information | 2004-08-16 | Paper |
| scientific article; zbMATH DE number 2086242 (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 |
Formalizing Belief Revision in Type Theory
Logic Journal of the IGPL | 2003-07-16 | Paper |
Revisiting the notion of function
The Journal of Logic and Algebraic Programming | 2003-06-25 | Paper |
Formalizing strong normalization proofs of explicit substitution calculi in ALF
Journal of Automated Reasoning | 2003-06-09 | Paper |
Pure Type Systems with de Bruijn Indices
The Computer Journal | 2002-12-19 | Paper |
Unification via the \(\lambda s_e\)-style of explicit substitutions
Logic Journal of the IGPL | 2002-06-19 | Paper |
| scientific article; zbMATH DE number 1692907 (Why is no real title available?) | 2002-01-21 | Paper |
Reviewing the classical and the de Bruijn notation for \(\lambda\)-calculus and pure type systems
Journal of Logic and Computation | 2001-10-16 | Paper |
Postponement, conservation and preservation of strong normalization for generalized reduction
Journal Of Logic And Computation | 2001-10-03 | Paper |
A correspondence between Martin-Löf type theory, the ramified theory of types and pure type systems
Journal of Logic, Language and Information | 2001-07-23 | Paper |
| scientific article; zbMATH DE number 1500561 (Why is no real title available?) | 2000-09-04 | Paper |
Relating the - and s-styles of explicit substitutions
Journal Of Logic And Computation | 2000-09-04 | Paper |
| scientific article; zbMATH DE number 1487841 (Why is no real title available?) | 2000-08-10 | Paper |
On -conversion in the -cube and the combination with abbreviations
Annals of Pure and Applied Logic | 2000-02-15 | Paper |
| scientific article; zbMATH DE number 1332643 (Why is no real title available?) | 1999-09-09 | Paper |
Bridging de Bruijn indices and variable names in explicit substitutions calculi
Logic Journal of the IGPL | 1999-06-21 | Paper |
| scientific article; zbMATH DE number 1088029 (Why is no real title available?) | 1998-04-01 | Paper |
Extending a λ-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms
Journal of Functional Programming | 1998-03-12 | Paper |
A useful \(\lambda\)-notation
Theoretical Computer Science | 1997-09-09 | Paper |
A unified approach to type theory through a refined -calculus
Theoretical Computer Science | 1997-02-27 | Paper |
Important Issues in Foundational Formalisms
Logic Journal of the IGPL | 1997-01-13 | Paper |
Canonical typing and ∏-conversion in the Barendregt Cube
Journal of Functional Programming | 1996-11-17 | Paper |
| scientific article; zbMATH DE number 877752 (Why is no real title available?) | 1996-07-16 | Paper |
The Barendregt cube with definitions and generalised reduction
Information and Computation | 1996-07-03 | Paper |
Refining reduction in the lambda calculus
Journal of Functional Programming | 1996-06-05 | Paper |
| scientific article; zbMATH DE number 847938 (Why is no real title available?) | 1996-03-19 | Paper |
A type free theory and collective/distributive predication
Journal of Logic, Language and Information | 1995-12-05 | Paper |
ON STEPWISE EXPLICIT SUBSTITUTION
International Journal of Foundations of Computer Science | 1994-04-27 | Paper |
Nominalization, predication and type containment
Journal of Logic, Language and Information | 1994-02-22 | Paper |
\(\lambda\)-terms, logic, determiners and quantifiers
Journal of Logic, Language and Information | 1994-02-22 | Paper |
Set Theory and Nominalization, Part II
Journal Of Logic And Computation | 1993-08-23 | Paper |
Set Theory and Nominalization, Part I
Journal Of Logic And Computation | 1993-06-29 | Paper |
A system at the cross-roads of functional and logic programming
Science of Computer Programming | 1993-05-16 | Paper |
Intersection Types via Finite-Set Declarations
(available as arXiv preprint) | N/A | Paper |
