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 description: 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 description: 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)
Temporal Type Theory
https://arxiv.org/abs/1710.10258
https://arxiv.org/abs/1710.10258
arXiv.org
Temporal Type Theory: A topos-theoretic approach to systems and behavior
This book introduces a temporal type theory, the first of its kind as far as we know. It is based on a standard core, and as such it can be formalized in a proof assistant such as Coq or Lean by...
Optimizing Optimal Reduction: A Type Inference Algorithm for Elementary Affine Logic
http://www.cs.unibo.it/~martini/papers-to-ftp/EA-typing.pdf
[Thanks to Parra]
http://www.cs.unibo.it/~martini/papers-to-ftp/EA-typing.pdf
[Thanks to Parra]
Lambda-calculus and Combinatory Logic
https://www.lama.univ-savoie.fr/pagesmembres/david/ftp/hindley.pdf
https://www.lama.univ-savoie.fr/pagesmembres/david/ftp/hindley.pdf
ICALP 2020 (http://econcs.pku.edu.cn/icalp2020/) and LICS 2020 (https://lics.siglog.org/lics20/) will take place in co-location from 8th till 12th of July 2020 in Beijing, China. The conferences will be preceded by two days of joint workshops, held on July 6th and 7th. We invite proposals of workshops affiliated with ICALP-LICS 2020 on all topics covered by ICALP and LICS, as well as other areas of theoretical computer science.
econcs.pku.edu.cn
ICALP 2020-EconCS@PKU