Linear Logic for Constructive Mathematics
https://arxiv.org/abs/1805.07518
https://arxiv.org/abs/1805.07518
arXiv.org
Affine logic for constructive mathematics
We show that numerous distinctive concepts of constructive mathematics arise automatically from an "antithesis" translation of affine logic into intuitionistic logic via a Chu/Dialectica...
Would aliens understand lambda calculus?
http://tomasp.net/blog/2018/alien-lambda-calculus/
[Thanks to Charlie Brown]
http://tomasp.net/blog/2018/alien-lambda-calculus/
[Thanks to Charlie Brown]
tomasp.net
Would aliens understand lambda calculus?
The question whether aliens would understand lambda calculus
is intriguing because it vividly formulates a fundamental question about our formal mathematical
knowledge. Are mathematical theories and results about them invented, i.e. constructed by
humans…
is intriguing because it vividly formulates a fundamental question about our formal mathematical
knowledge. Are mathematical theories and results about them invented, i.e. constructed by
humans…
Rewriting Type Theory
https://jesper.sikanda.be/posts/rewriting-type-theory.html
https://jesper.sikanda.be/posts/rewriting-type-theory.html
Formalizing ARM's Architecture Specification Language
https://alastairreid.github.io/specification_languages/
https://alastairreid.github.io/specification_languages/
alastairreid.github.io
ARM's Architecture Specification Language
What language should you write a specification in? Should you use the language
supported by your favourite verification tool (HOL, Verilog, …)?
Or should you write it in a DSL and translate that to whatever your
verification tool needs?
supported by your favourite verification tool (HOL, Verilog, …)?
Or should you write it in a DSL and translate that to whatever your
verification tool needs?
Reposting those introductory resources... Definitely worth taking a look at at least some of them
Forwarded from Pure & constructive mathematics in theory and use
[MLTT resources]
The original notes: https://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-retypeset-1984.pdf
A formal overview: https://ncatlab.org/nlab/show/Martin-L%C3%B6f+dependent+type+theory
Another denoscription: http://www.cse.chalmers.se/~peterd/papers/IntuitionisticTypeTheory150505.pdf
Programming in Martin-Löf type theory: https://www.dimap.ufrn.br/~regivan/pub/Programming_In_Martin_Loef_Type_Theory.pdf
[Resources for MLTT or similar about specific languages:]
Logic and Proof in Lean: https://leanprover.github.io/logic_and_proof/
General Theorem Proving in Lean: https://leanprover.github.io/theorem_proving_in_lean/
Programming Language Foundations in Agda: https://plfa.github.io/
Software foundations (based on Coq): https://softwarefoundations.cis.upenn.edu/current/index.html
The Nuprl Proof Development System: http://www.nuprl.org/book/
[HoTT resources]
The HoTT Book: https://homotopytypetheory.org/book/
HoTT in Agda: https://github.com/HoTT/HoTT-Agda
HoTT in Coq: https://github.com/HoTT/HoTT
The CoqHoTT project: http://coqhott.gforge.inria.fr/
Cubical type theory: https://arxiv.org/abs/1611.02108
Cubical type theory as Agda extension: https://agda.readthedocs.io/en/latest/language/cubical.html
Cubical Agda library: https://github.com/agda/cubical
The main implementation: https://github.com/mortberg/cubicaltt
An introduction to cubicaltt: https://homotopytypetheory.org/2017/09/16/a-hands-on-introduction-to-cubicaltt/
The original notes: https://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-retypeset-1984.pdf
A formal overview: https://ncatlab.org/nlab/show/Martin-L%C3%B6f+dependent+type+theory
Another denoscription: http://www.cse.chalmers.se/~peterd/papers/IntuitionisticTypeTheory150505.pdf
Programming in Martin-Löf type theory: https://www.dimap.ufrn.br/~regivan/pub/Programming_In_Martin_Loef_Type_Theory.pdf
[Resources for MLTT or similar about specific languages:]
Logic and Proof in Lean: https://leanprover.github.io/logic_and_proof/
General Theorem Proving in Lean: https://leanprover.github.io/theorem_proving_in_lean/
Programming Language Foundations in Agda: https://plfa.github.io/
Software foundations (based on Coq): https://softwarefoundations.cis.upenn.edu/current/index.html
The Nuprl Proof Development System: http://www.nuprl.org/book/
[HoTT resources]
The HoTT Book: https://homotopytypetheory.org/book/
HoTT in Agda: https://github.com/HoTT/HoTT-Agda
HoTT in Coq: https://github.com/HoTT/HoTT
The CoqHoTT project: http://coqhott.gforge.inria.fr/
Cubical type theory: https://arxiv.org/abs/1611.02108
Cubical type theory as Agda extension: https://agda.readthedocs.io/en/latest/language/cubical.html
Cubical Agda library: https://github.com/agda/cubical
The main implementation: https://github.com/mortberg/cubicaltt
An introduction to cubicaltt: https://homotopytypetheory.org/2017/09/16/a-hands-on-introduction-to-cubicaltt/
A Categorical Theory of Patches
https://www.youtube.com/watch?v=SnRFGZYo-xI
https://www.youtube.com/watch?v=SnRFGZYo-xI
YouTube
A Categorical Theory of Patches
When working with distant collaborators on the same documents, one often uses a version control system, which is a program tracking the history of files and helping importing modifications brought by others as patches. The implementation of such a system…
Cubical Methods to HoTT/UF
http://staff.math.su.se/anders.mortberg/papers/cubicalmethods.pdf
http://staff.math.su.se/anders.mortberg/papers/cubicalmethods.pdf
Metis Theorem Prover
http://www.gilith.com/metis/
http://www.gilith.com/metis/
Practical Foundations for Programming Languages (Second Edition): Bob Harper
https://www.cs.cmu.edu/~rwh/pfpl/
https://www.cs.cmu.edu/~rwh/pfpl/
The MMT Language and System
https://uniformal.github.io/
Imagine model theory, but you can choose the logic, the concept of homomorphism is internal to everything, there is a proof checker and a IDE.
This is close to being the hottest concept I ever saw.
https://uniformal.github.io/
Imagine model theory, but you can choose the logic, the concept of homomorphism is internal to everything, there is a proof checker and a IDE.
This is close to being the hottest concept I ever saw.
MultiMLton: A Multicore-Aware Runtime for Standard ML
https://cse.buffalo.edu/~lziarek/JFP_MultiMLton.pdf
https://cse.buffalo.edu/~lziarek/JFP_MultiMLton.pdf
On a Category of Cluster Algebras
https://arxiv.org/pdf/1201.5986.pdf
https://arxiv.org/pdf/1201.5986.pdf
Building Type Theories 1: Induction-Recursion
https://sofiafaro.wordpress.com/2019/11/06/building-type-theories-1/
https://sofiafaro.wordpress.com/2019/11/06/building-type-theories-1/
Sofia Faro
Building Type Theories 1: Induction-Recursion
I want to show you a technique for building a new type theory quickly. I use it to test and refine type theoretic ideas, without spending too much time. We’re going to build a small type theo…
Unix System Programming with Standard ML
http://mlton.org/References.attachments/Shipman02.pdf
Not exactly related to this channel, but probably useful for some viewing it
http://mlton.org/References.attachments/Shipman02.pdf
Not exactly related to this channel, but probably useful for some viewing it
John_H_Reppy_Concurrent_Programming.pdf
891 KB
Concurrent Programming in Standard ML (1999/2007)