| Publication | Date of Publication | Type |
|---|
An implicit particle code with \textit{exact} energy and charge conservation for studies of dense plasmas in axisymmetric geometries
Journal of Computational Physics | 2024-11-15 | Paper |
| Monoid Theory in Alonzo: A Little Theories Formalization in Simple Type Theory | 2023-12-09 | Paper |
| IMPS : An interactive mathematical proof system | 2023-04-28 | Paper |
Simple Type Theory
Computer Science Foundations and Applied Logic | 2023-04-21 | Paper |
Redex capturing in term graph rewriting (concise version)
Rewriting Techniques and Applications | 2022-12-09 | Paper |
Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge
The Mathematical Intelligencer | 2021-04-19 | Paper |
Leveraging the information contained in theory presentations
(available as arXiv preprint) | 2021-01-20 | Paper |
Towards specifying symbolic computation
(available as arXiv preprint) | 2020-01-22 | Paper |
IMPS: An updated system description
Automated Deduction — Cade-13 | 2019-01-15 | Paper |
Biform theories: project description
(available as arXiv preprint) | 2018-10-18 | Paper |
HOL Light QE
(available as arXiv preprint) | 2018-10-04 | Paper |
| A new style of mathematical proof | 2018-08-17 | Paper |
| A New Style of Proof for Mathematics Organized as a Network of Axiomatic Theories | 2018-06-03 | Paper |
Incorporating quotation and evaluation into Church's type theory
Information and Computation | 2018-05-30 | Paper |
Formalizing mathematical knowledge as a biform theory graph: a case study
(available as arXiv preprint) | 2017-07-21 | Paper |
Theory morphisms in Church's type theory with quotation and evaluation
(available as arXiv preprint) | 2017-07-21 | Paper |
Incorporating quotation and evaluation into Church's type theory: syntax and semantics
Lecture Notes in Computer Science | 2016-08-30 | Paper |
MKM
ACM SIGSAM Bulletin | 2016-07-18 | Paper |
Realms: a structure for consolidating knowledge about mathematical theories
Lecture Notes in Computer Science | 2014-08-07 | Paper |
Panoptes: an exploration tool for formal proofs
Electronic Notes in Theoretical Computer Science | 2014-06-27 | Paper |
| Simple Type Theory with Undefinedness, Quotation, and Evaluation | 2014-06-25 | Paper |
The formalization of syntax-based mathematical algorithms using quotation and evaluation
Lecture Notes in Computer Science | 2013-08-09 | Paper |
| Chiron: A Set Theory with Types, Undefinedness, Quotation, and Evaluation | 2013-05-27 | Paper |
MathScheme: project description
Lecture Notes in Computer Science | 2011-07-29 | Paper |
Andrews' type theory with undefinedness
(available as arXiv preprint) | 2011-03-30 | Paper |
A Review of Mathematical Knowledge Management
Lecture Notes in Computer Science | 2009-07-09 | Paper |
High-Level Theories
Lecture Notes in Computer Science | 2009-01-27 | Paper |
The seven virtues of simple type theory
Journal of Applied Logic | 2008-09-23 | Paper |
Biform Theories in Chiron
Towards Mechanized Mathematical Assistants | 2007-11-28 | Paper |
A Rational Reconstruction of a System for Experimental Mathematics
Towards Mechanized Mathematical Assistants | 2007-11-28 | Paper |
Automated Reasoning
Lecture Notes in Computer Science | 2007-09-25 | Paper |
An overview of a formal framework for managing mathematics
Annals of Mathematics and Artificial Intelligence | 2003-06-09 | Paper |
| A formal framework for managing mathematics | 2002-02-14 | Paper |
STMM: A set theory for mechanized mathematics
Journal of Automated Reasoning | 2001-11-07 | Paper |
A set theory with support for partial functions
Studia Logica | 2001-07-26 | Paper |
| scientific article; zbMATH DE number 1614690 (Why is no real title available?) | 2001-07-05 | Paper |
The Kreisel length-of-proof problem
Annals of Mathematics and Artificial Intelligence | 1997-05-13 | Paper |
A simple type theory with partial functions and subtypes
Annals of Pure and Applied Logic | 1996-05-13 | Paper |
A unification-theoretic method for investigating the \(k\)-provability problem
Annals of Pure and Applied Logic | 1992-06-25 | Paper |
Simple second-order languages for which unification is undecidable
Theoretical Computer Science | 1991-01-01 | Paper |
REDEX CAPTURING IN TERM GRAPH REWRITING
International Journal of Foundations of Computer Science | 1990-01-01 | Paper |
A partial functions version of Church's simple theory of types
Journal of Symbolic Logic | 1990-01-01 | Paper |
A unification algorithm for second-order monadic terms
Annals of Pure and Applied Logic | 1988-01-01 | Paper |
