String Diagrams for Optics
https://arxiv.org/pdf/2002.11480.pdf
https://arxiv.org/pdf/2002.11480.pdf
Fundamentals of Model Theory
http://www.math.toronto.edu/weiss/model_theory.pdf
http://www.math.toronto.edu/weiss/model_theory.pdf
Introduction to Mathematical Logic
https://www.karlin.mff.cuni.cz/~krajicek/mendelson.pdf
https://www.karlin.mff.cuni.cz/~krajicek/mendelson.pdf
Sets, Classes and Categories
http://philsci-archive.pitt.edu/1372/1/SetClassCat.PDF
http://philsci-archive.pitt.edu/1372/1/SetClassCat.PDF
The Axiom of Countable Choice in Topology
http://www.mat.uc.pt/~ggutc/teses/teseingles.pdf
http://www.mat.uc.pt/~ggutc/teses/teseingles.pdf
Diagram Generator for Consequences of the Axiom of Choice
https://cgraph.inters.co/
https://cgraph.inters.co/
Ordinal Logic and the Characterization of Informal Concepts of Proof
https://web.archive.org/web/20170118205333/http://www.mathunion.org/ICM/ICM1958/Main/icm1958.0289.0299.ocr.pdf
https://web.archive.org/web/20170118205333/http://www.mathunion.org/ICM/ICM1958/Main/icm1958.0289.0299.ocr.pdf
Categorical Programming with Inductive and Coinductive Types
https://kodu.ut.ee/~varmo/papers/thesis.pdf
https://kodu.ut.ee/~varmo/papers/thesis.pdf
Formal Derivation of a Scheme Computer
https://legacy.cs.indiana.edu/ftp/techreports/TR544.pdf
Slightly off topic, but somewhat interesting
https://legacy.cs.indiana.edu/ftp/techreports/TR544.pdf
Slightly off topic, but somewhat interesting
Sets for Mathematics
http://patryshev.com/books/Sets%20for%20Mathematics.pdf
http://patryshev.com/books/Sets%20for%20Mathematics.pdf
Foundations of Algebraic Geometry
http://math.stanford.edu/~vakil/216blog/FOAGnov1817public.pdf
http://math.stanford.edu/~vakil/216blog/FOAGnov1817public.pdf
Design Patterns as Higher-Order Datatype-Generic Programs
http://www.cs.ox.ac.uk/jeremy.gibbons/publications/hodgp.pdf
http://www.cs.ox.ac.uk/jeremy.gibbons/publications/hodgp.pdf
Logic-Free Formalisations of Recursive Arithmetic
https://www.mscand.dk/article/view/10412/8433
https://www.mscand.dk/article/view/10412/8433
Purely Functional Data Structures
http://www.cs.cmu.edu/~rwh/theses/okasaki.pdf
http://www.cs.cmu.edu/~rwh/theses/okasaki.pdf
About the completeness of a certain system of integer arithmetic in which addition is the only operation (translated, with additional remarks)
https://cs.fit.edu/~ryan/papers/presburger.pdf
https://cs.fit.edu/~ryan/papers/presburger.pdf
Complexity Hierarchies beyond ELEMENTARY
https://arxiv.org/pdf/1312.5686.pdf
https://arxiv.org/pdf/1312.5686.pdf
The Realm of Ordinal Analysis
https://www1.maths.leeds.ac.uk/~rathjen/realm.pdf
https://www1.maths.leeds.ac.uk/~rathjen/realm.pdf
Valery Isaev - Arend Proof Assistant.pdf
140.2 KB
Arend Proof Assistant
Andrea Vezzosi - Indexed Families in Cubical Agda.pdf
74 KB
Indexed Families' computation in Cubical Agda
An Introduction to Proof Theory
http://www.math.ucsd.edu/~sbuss/ResearchWeb/handbookI/ChapterI.pdf
http://www.math.ucsd.edu/~sbuss/ResearchWeb/handbookI/ChapterI.pdf