Type and proof

This is the latex source of Type and proof, a short article about logic, type system, lambda calculus, and curry howard isomorphism.

There may be some mistakes and it is not completed yet. Issues and pull requests are welcomed!

TODO

• denotational semantic of UTLC and STLC
• logical relation and its applications
• C-H isomorphism under sequent calculus
• type inference of STLC
• type checking VS. proof checking
• \beta and \eta reduction VS. prooving
• cut elimination and it's role in C-H isomorphism
• intro to proof search
• intro to category theory
• algebra semantic of logic and STLC
• intro to lambda cube
• linear logic and lienar type
• substructural logic and substructural type
• focusing/polarizing in type theory
• First order logic
• basic model theory

Contributors

https://github.com/OpenPAL/TypeAndProof/graphs/contributors

How to publish the PDF

https://openpal.github.io/TypeAndProof/ is where we publish. Here are several steps:

1. Generate the PDF file from source
2. Clone another copy of this repo, named like TypeAndProof-www
3. In that new repo, check out into the gh-pages branch
4. Copy the new version of PDF here
5. git add --all; git commit -m "Update PDF"
6. Make a PR or something to that particular branch