| Publication | Date of Publication | Type |
|---|
An Introduction to Lorenzen's ‘Algebraic and Logistic Investigations on Free Lattices’ (1951) (edit)
History and Philosophy of Logic | 2026-03-31 | Paper |
| Realizability at work: separating two constructive notions of finiteness | 2026-02-20 | Paper |
| A normalizing computation rule for propositional extensionality in higher-order minimal logic | 2026-02-20 | Paper |
Controlling unfolding in type theory
Mathematical Structures in Computer Science | 2025-12-30 | Paper |
A foundation for synthetic algebraic geometry
Mathematical Structures in Computer Science | 2025-03-04 | Paper |
| A variation of Reynolds-Hurkens paradox | 2025-02-07 | Paper |
| Type theory with explicit universe polymorphism | 2024-11-26 | Paper |
Infinite objects in type theory
Lecture Notes in Computer Science | 2023-12-08 | Paper |
| Heitman dimension of distributive lattices and commutative rings | 2023-12-01 | Paper |
| A variation of Reynolds-Hurkens Paradox | 2023-08-31 | Paper |
Reduction Free Normalisation for a proof irrelevant type of propositions
Logical Methods in Computer Science | 2023-08-26 | Paper |
Constructive Algebra and Point-Free Topology
Handbook of Constructive Mathematics | 2023-08-11 | Paper |
Constructive Theory of Ordinals
Mathematics for Computation (M4C) | 2023-08-04 | Paper |
| Constructive Remarks on Azumaya Algebra | 2023-06-30 | Paper |
| A Foundation for Synthetic Algebraic Geometry | 2023-06-30 | Paper |
Lorenzen's Proof of Consistency for Elementary Number Theory
History and Philosophy of Logic | 2023-06-14 | Paper |
Some remarks about normal rings
(available as arXiv preprint) | 2022-10-29 | Paper |
| scientific article; zbMATH DE number 7559277 (Why is no real title available?) | 2022-07-18 | Paper |
On generalized algebraic theories and categories with families
Mathematical Structures in Computer Science | 2022-06-24 | Paper |
Constructive sheaf models of type theory
Mathematical Structures in Computer Science | 2022-06-24 | Paper |
Formal Topology and Univalent Foundations
Proof and Computation II | 2022-06-17 | Paper |
Loop-checking and the uniform word problem for join-semilattices with an inflationary endomorphism
Theoretical Computer Science | 2022-04-07 | Paper |
Canonicity and homotopy canonicity for cubical type theory
(available as arXiv preprint) | 2022-02-09 | Paper |
| Canonicity and homotopy canonicity for cubical type theory | 2022-02-09 | Paper |
Lorenzen and constructive mathematics
Paul Lorenzen -- Mathematician and Logician | 2022-01-27 | Paper |
Regular entailment relations
Paul Lorenzen -- Mathematician and Logician | 2022-01-27 | Paper |
Syntax and models of Cartesian cubical type theory
Mathematical Structures in Computer Science | 2022-01-20 | Paper |
| A sheaf model of the algebraic closure | 2021-06-24 | Paper |
A sheaf model of the algebraic closure
(available as arXiv preprint) | 2021-06-24 | Paper |
| Constructive basic theory of central simple algebras | 2021-02-25 | Paper |
On higher inductive types in cubical type theory
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science | 2021-01-20 | Paper |
Inner Models of Univalence
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science | 2021-01-20 | Paper |
| Stack semantics of type theory | 2021-01-19 | Paper |
Stack semantics of type theory
(available as arXiv preprint) | 2021-01-19 | Paper |
A Note on Generalized Algebraic Theories and Categories with Families
(available as arXiv preprint) | 2020-12-15 | Paper |
scientific article; zbMATH DE number 7225974 (Why is no real title available?)
(available as arXiv preprint) | 2020-07-30 | Paper |
| scientific article; zbMATH DE number 7225974 (Why is no real title available?) | 2020-07-30 | Paper |
| Lorenzen's proof of consistency for elementary number theory [with an edition and translation of "Ein halbordnungstheoretischer Widerspruchsfreiheitsbeweis''] | 2020-06-16 | Paper |
Some remarks about normal rings
Concepts of Proof in Mathematics, Philosophy, and Computer Science | 2020-04-03 | Paper |
Skolem’s Theorem in Coherent Logic
Fundamenta Informaticae | 2020-01-24 | Paper |
Regular entailment relations
(available as arXiv preprint) | 2019-12-19 | Paper |
Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality
(available as arXiv preprint) | 2019-11-19 | Paper |
Lattice-ordered groups generated by an ordered group and regular systems of ideals
Rocky Mountain Journal of Mathematics | 2019-10-04 | Paper |
Lattice-ordered groups generated by an ordered group and regular systems of ideals
Rocky Mountain Journal of Mathematics | 2019-10-04 | Paper |
| A formal proof of Sasaki-Murao algorithm | 2019-09-18 | Paper |
The univalence axiom in cubical sets
Journal of Automated Reasoning | 2019-08-21 | Paper |
An adequacy theorem for dependent type theory
Theory of Computing Systems | 2019-07-04 | Paper |
Canonicity and normalization for dependent type theory
Theoretical Computer Science | 2019-06-18 | Paper |
An application of constructive completeness
Lecture Notes in Computer Science | 2019-01-15 | Paper |
| R\'esolutions libres finies. M\'ethodes constructives | 2018-11-05 | Paper |
Syntactic forcing models for coherent logic
Indagationes Mathematicae. New Series | 2018-10-08 | Paper |
Combinatorial topology and constructive mathematics
Indagationes Mathematicae. New Series | 2018-10-08 | Paper |
Cubical type theory: a constructive interpretation of the univalence axiom
(available as arXiv preprint) | 2018-08-13 | Paper |
An elementary proof of Wiebe's theorem
Journal of Algebra | 2018-03-01 | Paper |
| Hidden constructions in abstract algebra, Krull Dimension, Going Up, Going Down | 2017-12-13 | Paper |
| Constructions cach\'ees en alg\`ebre abstraite. Dimension de Krull, Going Up, Going Down (revised version, 2008) | 2017-12-13 | Paper |
Constructive topology and combinatorics
Lecture Notes in Computer Science | 2017-11-17 | Paper |
| An introduction to Lorenzen's "Algebraic and logistic investigations on free lattices'' (1951) | 2017-11-14 | Paper |
| The independence of Markov's principle in type theory | 2017-10-17 | Paper |
The independence of Markov's principle in type theory
(available as arXiv preprint) | 2017-10-12 | Paper |
| Type theory and formalisation of mathematics | 2017-08-22 | Paper |
| The Ackermann Award 2016 | 2017-07-19 | Paper |
| Non-constructivity in Kan simplicial sets | 2017-07-12 | Paper |
Notions of anonymous existence in Martin-Löf type theory
(available as arXiv preprint) | 2017-05-08 | Paper |
| scientific article; zbMATH DE number 6694181 (Why is no real title available?) | 2017-03-13 | Paper |
| Theory of dependent types and axiom of univalence | 2017-03-02 | Paper |
A presheaf model of parametric type theory
Electronic Notes in Theoretical Computer Science | 2016-12-16 | Paper |
A generalization of the Takeuti-Gandy interpretation
Mathematical Structures in Computer Science | 2016-07-27 | Paper |
Anneaux à diviseurs et anneaux de Krull (une approche constructive)
Communications in Algebra | 2016-04-25 | Paper |
Computing persistent homology within Coq/SSReflect
ACM Transactions on Computational Logic | 2015-09-17 | Paper |
A computational interpretation of forcing in type theory
Epistemology versus Ontology | 2015-06-05 | Paper |
Recursive Functions and Constructive Mathematics
Logic, Epistemology, and the Unity of Science | 2015-05-19 | Paper |
A Kripke model for simplicial sets
Theoretical Computer Science | 2015-02-24 | Paper |
Dynamic Newton-Puiseux theorem
Journal of Logic and Analysis | 2014-11-20 | Paper |
Isomorphism is equality
Indagationes Mathematicae. New Series | 2014-09-03 | Paper |
Revisiting Zariski main theorem from a constructive point of view
Journal of Algebra | 2014-08-28 | Paper |
Constructive algebra
La Gaceta de la Real Sociedad Matemática Española | 2014-08-28 | Paper |
A constructive version of Laplace's proof on the existence of complex roots
Journal of Algebra | 2013-10-28 | Paper |
Generalizations of Hedberg's theorem
Lecture Notes in Computer Science | 2013-06-28 | Paper |
Coherent and Strongly Discrete Rings in Type Theory
Certified Programs and Proofs | 2013-04-19 | Paper |
About Goodman's theorem
Annals of Pure and Applied Logic | 2013-03-15 | Paper |
Constructive theory of Banach algebras
Journal of Logic and Analysis | 2012-12-17 | Paper |
Unique paths as formal points
Journal of Logic and Analysis | 2012-12-17 | Paper |
A constructive proof of Simpson's rule
Journal of Logic and Analysis | 2012-12-17 | Paper |
| The Ackermann Award 2012. | 2012-11-22 | Paper |
Stop when you are almost-full. Adventures in constructive termination
Interactive Theorem Proving | 2012-09-20 | Paper |
Constructive finite free resolutions
Manuscripta Mathematica | 2012-02-14 | Paper |
A Decision Procedure for Regular Expression Equivalence in Type Theory
Certified Programs and Proofs | 2011-11-22 | Paper |
Metric complements of overt closed sets
Mathematical Logic Quarterly | 2011-09-27 | Paper |
Games with 1-backtracking
Annals of Pure and Applied Logic | 2011-08-26 | Paper |
A modular type-checking algorithm for type theory with singleton types and proof irrelevance
Logical Methods in Computer Science | 2011-05-26 | Paper |
| scientific article; zbMATH DE number 5831413 (Why is no real title available?) | 2011-01-03 | Paper |
A note on forcing and type theory
Fundamenta Informaticae | 2011-01-03 | Paper |
Curves and coherent Prüfer rings
Journal of Symbolic Computation | 2010-11-19 | Paper |
Spectral schemes as ringed lattices
Annals of Mathematics and Artificial Intelligence | 2010-03-19 | Paper |
| A simple type-theoretic language: Mini-TT | 2010-02-05 | Paper |
Constructive Gelfand duality for C*-algebras
Mathematical Proceedings of the Cambridge Philosophical Society | 2009-10-19 | Paper |
| scientific article; zbMATH DE number 5604075 (Why is no real title available?) | 2009-09-15 | Paper |
A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance
Lecture Notes in Computer Science | 2009-07-07 | Paper |
| scientific article; zbMATH DE number 5575850 (Why is no real title available?) | 2009-07-06 | Paper |
CONSTRUCTIVE KRULL DIMENSION I: INTEGRAL EXTENSIONS
Journal of Algebra and its Applications | 2009-04-28 | Paper |
Integrals and valuations
Journal of Logic and Analysis | 2009-04-15 | Paper |
| Dimension de Heitmann des treillis distributifs et des anneaux commutatifs | 2009-04-14 | Paper |
Dimension de Heitmann des treillis distributifs et des anneaux commutatifs
(available as arXiv preprint) | 2009-04-14 | Paper |
Space of valuations
Annals of Pure and Applied Logic | 2009-03-25 | Paper |
Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory
Lecture Notes in Computer Science | 2008-08-28 | Paper |
| Kolmogorov's contribution to intuitionistic logic | 2008-06-27 | Paper |
A note on the axiomatisation of real numbers
MLQ | 2008-06-12 | Paper |
Automating Coherent Logic
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-27 | Paper |
On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory
Functional and Logic Programming | 2008-04-11 | Paper |
Constructive Mathematics and Functional Programming (Abstract)
Programming Languages and Systems | 2008-04-11 | Paper |
A proof of strong normalisation using domain theory
Logical Methods in Computer Science | 2008-04-01 | Paper |
| The projective spectrum as a distributive lattice | 2008-01-18 | Paper |
Towards Constructive Homological Algebra in Type Theory
Towards Mechanized Mathematical Assistants | 2007-11-28 | Paper |
| Formal topology and constructive mathematics: the Gelfand and Stone-Yosida representation theorems | 2007-10-15 | Paper |
Formal topology and constructive mathematics: the Gelfand and Stone-Yosida representation theorems
(available as arXiv preprint) | 2007-10-15 | Paper |
| The completeness of typing for context-semantics | 2007-07-20 | Paper |
| scientific article; zbMATH DE number 5173450 (Why is no real title available?) | 2007-07-20 | Paper |
A logical approach to abstract algebra
Mathematical Structures in Computer Science | 2007-02-09 | Paper |
On seminormality
Journal of Algebra | 2006-12-07 | Paper |
A Short Proof for the Krull Dimension of a Polynomial Ring
The American Mathematical Monthly | 2006-12-05 | Paper |
Types for Proofs and Programs
Lecture Notes in Computer Science | 2006-11-13 | Paper |
Frontiers of Combining Systems
Lecture Notes in Computer Science | 2006-10-10 | Paper |
| scientific article; zbMATH DE number 5046775 (Why is no real title available?) | 2006-08-16 | Paper |
Remarks on the equational theory of non-normalizing pure type systems
Journal of Functional Programming | 2006-03-22 | Paper |
Geometric Hahn-Banach theorem
Mathematical Proceedings of the Cambridge Philosophical Society | 2006-03-22 | Paper |
| scientific article; zbMATH DE number 2247262 (Why is no real title available?) | 2006-01-16 | Paper |
New Computational Paradigms
Lecture Notes in Computer Science | 2006-01-11 | Paper |
Typed Lambda Calculi and Applications
Lecture Notes in Computer Science | 2005-11-11 | Paper |
Typed Lambda Calculi and Applications
Lecture Notes in Computer Science | 2005-11-11 | Paper |
A nilregular element property
Archiv der Mathematik | 2005-08-17 | Paper |
A constructive proof of the Peter-Weyl theorem
MLQ | 2005-08-01 | Paper |
| scientific article; zbMATH DE number 2185652 (Why is no real title available?) | 2005-07-04 | Paper |
| scientific article; zbMATH DE number 2182489 (Why is no real title available?) | 2005-06-23 | Paper |
A note on measures with values in a partially ordered vector space
Positivity | 2005-06-13 | Paper |
About Stone's notion of spectrum
Journal of Pure and Applied Algebra | 2005-04-18 | Paper |
| scientific article; zbMATH DE number 2155188 (Why is no real title available?) | 2005-04-11 | Paper |
Generating non-Noetherian modules constructively
Manuscripta Mathematica | 2005-02-02 | Paper |
Proof-theoretical analysis of order relations
Archive for Mathematical Logic | 2004-12-16 | Paper |
Remarks on the equational theory of non-normalizing pure type systems
Journal of Functional Programming | 2004-09-24 | Paper |
| scientific article; zbMATH DE number 2090721 (Why is no real title available?) | 2004-08-13 | Paper |
Hidden constructions in abstract algebra. Krull Dimension of distributive lattices and commutative rings
(available as arXiv preprint) | 2004-08-09 | Paper |
| scientific article; zbMATH DE number 2085166 (Why is no real title available?) | 2004-08-09 | Paper |
| scientific article; zbMATH DE number 2077110 (Why is no real title available?) | 2004-07-01 | Paper |
| scientific article; zbMATH DE number 2061705 (Why is no real title available?) | 2004-03-22 | Paper |
On a theorem of Kronecker about algebraic varieties
Comptes Rendus. Mathématique. Académie des Sciences, Paris | 2004-03-15 | Paper |
Inductively generated formal topologies.
Annals of Pure and Applied Logic | 2003-11-25 | Paper |
Metric Boolean algebras and constructive measure theory
Archive for Mathematical Logic | 2003-09-16 | Paper |
Compact spaces and distributive lattices.
Journal of Pure and Applied Algebra | 2003-09-15 | Paper |
A syntactical proof of the Marriage Lemma.
Theoretical Computer Science | 2003-01-21 | Paper |
Valuations and Dedekind's Prague theorem
Journal of Pure and Applied Algebra | 2002-04-10 | Paper |
| scientific article; zbMATH DE number 1722646 (Why is no real title available?) | 2002-03-21 | Paper |
| scientific article; zbMATH DE number 1420784 (Why is no real title available?) | 2002-02-17 | Paper |
| scientific article; zbMATH DE number 1670483 (Why is no real title available?) | 2001-12-03 | Paper |
Formal topologies on the set of first-order formulae
Journal of Symbolic Logic | 2001-07-22 | Paper |
| scientific article; zbMATH DE number 1497758 (Why is no real title available?) | 2001-03-06 | Paper |
Intuitionistic choice and classical logic
Archive for Mathematical Logic | 2000-11-05 | Paper |
| scientific article; zbMATH DE number 1420837 (Why is no real title available?) | 2000-03-22 | Paper |
A new method for establishing conservativity of classical systems over their intuitionistic version
Mathematical Structures in Computer Science | 1999-11-25 | Paper |
| scientific article; zbMATH DE number 1302057 (Why is no real title available?) | 1999-10-05 | Paper |
A Boolean model of ultrafilters
Annals of Pure and Applied Logic | 1999-09-22 | Paper |
On the computational content of the axiom of choice
Journal of Symbolic Logic | 1999-06-21 | Paper |
| scientific article; zbMATH DE number 1223620 (Why is no real title available?) | 1999-04-19 | Paper |
| scientific article; zbMATH DE number 1241698 (Why is no real title available?) | 1999-01-18 | Paper |
Two applications of Boolean models
Archive for Mathematical Logic | 1998-08-10 | Paper |
Intuitionistic model constructions and normalization proofs
MSCS. Mathematical Structures in Computer Science | 1998-03-23 | Paper |
Minimal invariant spaces in formal topology
Journal of Symbolic Logic | 1998-03-17 | Paper |
| scientific article; zbMATH DE number 952103 (Why is no real title available?) | 1997-03-13 | Paper |
A constructive topological proof of van der Waerden's theorem
Journal of Pure and Applied Algebra | 1996-07-16 | Paper |
An algorithm for type-checking dependent types
Science of Computer Programming | 1996-07-03 | Paper |
| scientific article; zbMATH DE number 814794 (Why is no real title available?) | 1996-04-16 | Paper |
A semantics of evidence for classical arithmetic
Journal of Symbolic Logic | 1996-01-21 | Paper |
An analysis of Ramsey's theorem
Information and Computation | 1995-11-09 | Paper |
| scientific article; zbMATH DE number 733401 (Why is no real title available?) | 1995-09-18 | Paper |
A-translation and looping combinators in pure type systems
Journal of Functional Programming | 1995-06-11 | Paper |
Another proof of the intuitionistic Ramsey theorem
Theoretical Computer Science | 1994-12-01 | Paper |
| scientific article; zbMATH DE number 517049 (Why is no real title available?) | 1994-09-11 | Paper |
| scientific article; zbMATH DE number 559219 (Why is no real title available?) | 1994-05-24 | Paper |
The paradox of trees in type theory
BIT | 1993-11-28 | Paper |
| scientific article; zbMATH DE number 65534 (Why is no real title available?) | 1992-09-27 | Paper |
An intuitionistic proof of Tychonoff's theorem
Journal of Symbolic Logic | 1992-09-27 | Paper |
| scientific article; zbMATH DE number 55171 (Why is no real title available?) | 1992-09-26 | Paper |
Inheritance as implicit coercion
Information and Computation | 1992-06-25 | Paper |
The Wiener lemma and certain of its generalizations
Bulletin of the American Mathematical Society | 1992-06-25 | Paper |
| scientific article; zbMATH DE number 4189687 (Why is no real title available?) | 1990-01-01 | Paper |
| scientific article; zbMATH DE number 4180771 (Why is no real title available?) | 1989-01-01 | Paper |
Categories of embeddings
Theoretical Computer Science | 1989-01-01 | Paper |
Domain theoretic models of polymorphism
Information and Computation | 1989-01-01 | Paper |
| scientific article; zbMATH DE number 4050971 (Why is no real title available?) | 1988-01-01 | Paper |
The calculus of constructions
Information and Computation | 1988-01-01 | Paper |
Extensional models for polymorphism
Theoretical Computer Science | 1988-01-01 | Paper |
| scientific article; zbMATH DE number 4035777 (Why is no real title available?) | 1987-01-01 | Paper |
| scientific article; zbMATH DE number 4047723 (Why is no real title available?) | 1987-01-01 | Paper |
| scientific article; zbMATH DE number 4019061 (Why is no real title available?) | 1987-01-01 | Paper |
| scientific article; zbMATH DE number 4057475 (Why is no real title available?) | 1986-01-01 | Paper |
| scientific article; zbMATH DE number 3928956 (Why is no real title available?) | 1985-01-01 | Paper |
A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
Journal of Symbolic Computation | 1985-01-01 | Paper |
| scientific article; zbMATH DE number 3933045 (Why is no real title available?) | 1984-01-01 | Paper |
The Regular Element Property in Constructive Mathematics
(available as arXiv preprint) | N/A | Paper |
