A suite of cool logic programs
https://xorshammer.com/2009/05/14/a-suite-of-cool-logic-programs/
https://xorshammer.com/2009/05/14/a-suite-of-cool-logic-programs/
XOR's Hammer
A Suite of Cool Logic Programs
You may have heard about the Tarski-Seidenberg theorem, which says that the first-order theory of the reals is decidable, that the first-order theory of the complex numbers is similarly decidable, …
The relative efficiency of propositional proof systems
https://www.cs.toronto.edu/~sacook/homepage/cook_reckhow.pdf
https://www.cs.toronto.edu/~sacook/homepage/cook_reckhow.pdf
Restricted Set-theoretic Definitions in Arithmetic
https://www.ams.org/journals/proc/1958-009-02/S0002-9939-1958-0093479-4/S0002-9939-1958-0093479-4.pdf
https://www.ams.org/journals/proc/1958-009-02/S0002-9939-1958-0093479-4/S0002-9939-1958-0093479-4.pdf
Real Analysis in Reverse
http://faculty.uml.edu/jpropp/reverse.pdf
http://faculty.uml.edu/jpropp/reverse.pdf
Unfolding Finitist Arithmetic
http://math.stanford.edu/~feferman/papers/UnfoldFA.pdf
http://math.stanford.edu/~feferman/papers/UnfoldFA.pdf
The Unfolding of Non-Finitist Airthmetic
http://math.stanford.edu/~feferman/papers/unfolding.pdf
http://math.stanford.edu/~feferman/papers/unfolding.pdf
Believing the Axioms
http://www.cs.umd.edu/~gasarch/BLOGPAPERS/belaxioms1.pdf
http://www.cs.umd.edu/~gasarch/BLOGPAPERS/belaxioms1.pdf
The Strength of Mac Lane Set Theory
https://www.dpmms.cam.ac.uk/~ardm/maclane.pdf
https://www.dpmms.cam.ac.uk/~ardm/maclane.pdf
A Univalent Universe in Finite Order Arithmetic
https://arxiv.org/pdf/1412.6714.pdf
https://arxiv.org/pdf/1412.6714.pdf
Rectangular Axioms, perfect set properties and decomposition
http://www.users.miamioh.edu/larsonpb/goedel.pdf
http://www.users.miamioh.edu/larsonpb/goedel.pdf
Number theory and elementary arithmetic
http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=0F5B8AAA8EBE01A962B6B0DAA8A7A873?doi=10.1.1.105.6509&rep=rep1&type=pdf
http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=0F5B8AAA8EBE01A962B6B0DAA8A7A873?doi=10.1.1.105.6509&rep=rep1&type=pdf
Cardinal Arithmetic in the style of Baron von Münchhausen
https://dspace.library.uu.nl/bitstream/handle/1874/33720/preprint272.pdf?sequence=1&isAllowed=y
https://dspace.library.uu.nl/bitstream/handle/1874/33720/preprint272.pdf?sequence=1&isAllowed=y
Nonstandard Models of Arithmetic
https://diagonalargument.com/mathnotes/nonstandard-models-of-arithmetic-the-series/
https://diagonalargument.com/mathnotes/nonstandard-models-of-arithmetic-the-series/
Diagonal Argument
Nonstandard Models of Arithmetic: The Series
John Baez and I have been conducting a conversation about nonstandard models of Peano arithmetic (PA). This page serves as an annotated table of contents, bibliography, and general repository for s…
What is effective transfinite recursion in reverse mathematics?
https://arxiv.org/pdf/2006.08953.pdf
https://arxiv.org/pdf/2006.08953.pdf
Representing contractive functions on streams
http://www.cs.nott.ac.uk/~pszgmh/contractive.pdf
http://www.cs.nott.ac.uk/~pszgmh/contractive.pdf
Type-Based Methods for Termination and Productivity in Coq
https://coq.inria.fr/files/coq5_submission_5.pdf
https://coq.inria.fr/files/coq5_submission_5.pdf
Integrating Dependent and Linear Types
https://www.cl.cam.ac.uk/~nk480/dlnl-paper.pdf
https://www.cl.cam.ac.uk/~nk480/dlnl-paper.pdf
A survey of compatibility logic
https://arxiv.org/abs/1612.04513
http://www.csc.villanova.edu/~japaridz/CL/
https://arxiv.org/abs/1612.04513
http://www.csc.villanova.edu/~japaridz/CL/
Strict Set (which Agda calls SSet) comes from 2-level type theory, see https://arxiv.org/pdf/1705.03307.pdf and https://arxiv.org/pdf/1604.03799.pdf)