Compiling with Classical Connectives
https://arxiv.org/abs/1907.13227
https://arxiv.org/abs/1907.13227
A simple model for quotient times
https://link.springer.com/chapter/10.1007/BFb0014055
[Thanks to T. Heindel]
https://link.springer.com/chapter/10.1007/BFb0014055
[Thanks to T. Heindel]
SpringerLink
A simple model for quotient types
We give an interpretation of quotient types within in a dependent type theory with an impredicative universe of propositions (Calculus of Constructions). In the model, type dependency arises only at...
Constructive reverse mathematics
https://arxiv.org/pdf/1804.05495.pdf
https://arxiv.org/pdf/1804.05495.pdf
Formal Reasoning About Programs
http://adam.chlipala.net/frap/frap_book.pdf
http://adam.chlipala.net/frap/frap_book.pdf
Persistent Homology - a Survey
https://www.maths.ed.ac.uk/~v1ranick/papers/edelhare.pdf
[Thanks to kl mw]
https://www.maths.ed.ac.uk/~v1ranick/papers/edelhare.pdf
[Thanks to kl mw]
Normal Derivability and First-Order Arithmetic
https://projecteuclid.org/download/pdf_1/euclid.ndjfl/1093883058
https://projecteuclid.org/download/pdf_1/euclid.ndjfl/1093883058
projecteuclid.org
Tosi : Normal derivability and first-order arithmetic.
Project Euclid - mathematics and statistics online
How to Write Seemingly Unhygienic and Referentially Opaque Macros with Syntax-rules
http://okmij.org/ftp/Scheme/Dirty-Macros.pdf
A bit more programming-related, but still close enough to matter :)
[Thanks to Freddie]
http://okmij.org/ftp/Scheme/Dirty-Macros.pdf
A bit more programming-related, but still close enough to matter :)
[Thanks to Freddie]
Fast and Loose Reasoning is Morally Correct
https://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loose.pdf
https://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loose.pdf
Understanding and Using Spector’s Bar Recursive Interpretation of Classical Analysis
https://www.eecs.qmul.ac.uk/~pbo/papers/paper011.pdf
https://www.eecs.qmul.ac.uk/~pbo/papers/paper011.pdf
Elements of Finite Model Theory
https://homepages.inf.ed.ac.uk/libkin/fmt/fmt.pdf
https://homepages.inf.ed.ac.uk/libkin/fmt/fmt.pdf
Model theory Notes
https://math.berkeley.edu/~scanlon/225af13lectures/ModelTheoryNotes.pdf
https://math.berkeley.edu/~scanlon/225af13lectures/ModelTheoryNotes.pdf
Small update on Multicore OCaml
https://discuss.ocaml.org/t/where-is-multicore-development-happening/4997/8?u=yawaramin
https://discuss.ocaml.org/t/where-is-multicore-development-happening/4997/8?u=yawaramin
OCaml
Where is Multicore development happening?
Hopefully this is a pretty simple question, with the first hunk of multicore support being submitted upstream in mid-2019, where is OCaml multicore development happening? Is it still at the ocamllabs repo? The last commit there is 2 months ago and looks like…
Lean versus Coq: The cultural chasm
https://artagnon.com/articles/leancoq
https://artagnon.com/articles/leancoq
From setoid hell to homotopy heaven? The role of extensionality in Type Theory
http://www.cs.nott.ac.uk/~psztxa/talks/types-17-hell.pdf
[Thanks to Elias]
http://www.cs.nott.ac.uk/~psztxa/talks/types-17-hell.pdf
[Thanks to Elias]
The Arend Theorem Prover - A Tutorial
https://arend-lang.github.io/documentation/tutorial
https://arend-lang.github.io/documentation/tutorial
Various new theorems in constructive univalent mathematics written in Agda
https://github.com/martinescardo/TypeTopology
https://github.com/martinescardo/TypeTopology
GitHub
GitHub - martinescardo/TypeTopology: Logical manifestations of topological concepts, and other things, via the univalent point…
Logical manifestations of topological concepts, and other things, via the univalent point of view. - martinescardo/TypeTopology
Felis: Common Category Theoretic Abstractions for Standard ML
https://github.com/Saityi/felis
https://github.com/Saityi/felis
GitHub
Saityi/felis
(⚠️ Work in Progress ⚠️) Category theoretic abstractions and implementations - Saityi/felis