-
Notifications
You must be signed in to change notification settings - Fork 0
/
notes.txt
29 lines (27 loc) · 1.19 KB
/
notes.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
COIC
----
https://en.wikipedia.org/wiki/Calculus_of_constructions
https://leanprover.github.io/theorem_proving_in_lean/#01_Introduction.html
http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf
https://softwarefoundations.cis.upenn.edu/current/ProofObjects.html
https://coq.inria.fr/refman/Reference-Manual006.html
https://hal.inria.fr/inria-00076023/document - an analysis of girard's paradox, T. coquand
http://www.cse.chalmers.se/~bengt/papers/hlcs.pdf
http://www4.di.uminho.pt/~mjf/pub/SFV-CIC-2up.pdf
SML
---
http://sml-family.org/Basis/
https://people.mpi-sws.org/~rossberg/sml.html
https://hal.inria.fr/hal-01094195/file/CIC.pdf
http://flint.cs.yale.edu/cs428/coq/doc/Reference-Manual006.html
http://www.cs.cornell.edu/courses/cs312/2006fa/recitations/rec08.html
http://mlton.org/Fixpoints
http://courses.cs.washington.edu/courses/cse341/04wi/lectures/09-ml-modules.html
http://www.cs.cmu.edu/~rwh/isml/book.pdf
https://www.cs.cmu.edu/~rwh/introsml/core/
http://www.ccs.neu.edu/home/matthias/BTML/SML/
https://thebreakfastpost.com/2015/06/10/standard-ml-and-how-im-compiling-it/
MISC
----
http://www.jfsowa.com/pubs/egtut.pdf
http://www.cs.cmu.edu/~twelf/guide-1-4/twelf.pdf