A Formally Verified Abstract Account of Gödel's Incompleteness Theorems
https://www21.in.tum.de/~traytel/papers/cade19-incompleteness/incompleteness.pdf
https://www21.in.tum.de/~traytel/papers/cade19-incompleteness/incompleteness.pdf
4_5831262430465884843.pdf
218.5 KB
Corecursion and coinduction: how they relate to recursion and induction
Three Equivalent Ordinal Notation Systems in Cubical Agda
https://arxiv.org/pdf/1904.10759.pdf
https://arxiv.org/pdf/1904.10759.pdf
Ordinals and Interactive Programs
https://pdfs.semanticscholar.org/89c9/a2bca07752f9ed631c304bad8c34c2b163a2.pdf
https://pdfs.semanticscholar.org/89c9/a2bca07752f9ed631c304bad8c34c2b163a2.pdf
4_5862880936021983758.pdf
1 MB
Fundamental Theorems in Mathematics (2019)
A tutorial implementation of a dependently typed Lambda Calculus
https://www.andres-loeh.de/LambdaPi/LambdaPi.pdf
[Thanks to Elias]
https://www.andres-loeh.de/LambdaPi/LambdaPi.pdf
[Thanks to Elias]
Self-Verifying Axiom Systems, the Incompleteness Theorem and Related Reflection Principles
https://www.cs.albany.edu/~dew/m/jsl1.pdf
https://www.cs.albany.edu/~dew/m/jsl1.pdf
Summary of Truth about Types
https://rakhim.org/summary-of-truth-about-types-a-talk-by-bartosz-milewski/
https://rakhim.org/summary-of-truth-about-types-a-talk-by-bartosz-milewski/
Categorical Semantics of Digital Circuits
https://www.cs.bham.ac.uk/~drg/papers/fmcad16.pdf
[Thanks to Victor]
https://www.cs.bham.ac.uk/~drg/papers/fmcad16.pdf
[Thanks to Victor]
Semantics of higher inductive types
https://arxiv.org/abs/1705.07088
https://arxiv.org/abs/1705.07088
Higher Inductive Types in Cubical Computational Type Theory
https://dl.acm.org/doi/pdf/10.1145/3290314
https://dl.acm.org/doi/pdf/10.1145/3290314
Ask @ice1000 anything about higher inductive types. Currently he's studying it in-depth. He'll be interested in explaining things to you.
Category Theory for Programmers
https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/
https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/
Bartosz Milewski's Programming Cafe
Category Theory for Programmers: The Preface
Table of Contents Part One Category: The Essence of Composition Types and Functions Categories Great and Small Kleisli Categories Products and Coproducts Simple Algebraic Data Types Functors Functo…
Easy.pdf
187.6 KB
Simple Easy! An implementation of dependent type lambda calculus
Summary of Truth about Types, a talk by Bartosz Milewski
https://rakhim.org/summary-of-truth-about-types-a-talk-by-bartosz-milewski/
https://rakhim.org/summary-of-truth-about-types-a-talk-by-bartosz-milewski/
Graph Representations for Higher-Order Logic and Theorem Proving
https://arxiv.org/abs/1905.10006
https://arxiv.org/abs/1905.10006
Generative Language Modeling for Automated Theorem Proving
https://arxiv.org/pdf/2009.03393.pdf
https://arxiv.org/pdf/2009.03393.pdf
Towards Finding Longer Proofs
https://arxiv.org/pdf/1905.13100.pdf
https://arxiv.org/pdf/1905.13100.pdf
HoTT-I, the underlying type theory of Arend
https://arxiv.org/abs/2004.14195
https://arxiv.org/abs/2004.14195
An illustration of Hopf fibration
https://twitter.com/vi_ne_te/status/1302273506055516161
https://twitter.com/vi_ne_te/status/1302273506055516161
Twitter
Vignette
https://t.co/6XnX9C6xRr