summaryrefslogtreecommitdiffstats
path: root/transp-inf110-02-typage.tex
Commit message (Expand)AuthorAgeFilesLines
* Hopefully unfsck the whole situation with CPS translation and typing.David A. Madore2023-12-141-45/+135
* Try to fix CPS transformation, but this is still broken. :-(David A. Madore2023-12-131-35/+39
* Change chapter title to include propositional calculus.David A. Madore2023-12-131-1/+1
* Add a few call/cc puzzles.David A. Madore2023-12-131-1/+18
* Many remarks on continuation-passing-style.David A. Madore2023-12-131-1/+86
* Applications of continuations.David A. Madore2023-12-131-2/+33
* Additional remark.David A. Madore2023-12-131-2/+14
* Systematization of continuation-passing-style.David A. Madore2023-12-131-0/+85
* Expand last example slightly.David A. Madore2023-12-121-1/+5
* Discuss continuation-passing-style.David A. Madore2023-12-121-2/+53
* Typing of call/cc.David A. Madore2023-12-121-1/+128
* A brief description of continuations and call/cc.David A. Madore2023-12-121-2/+111
* Slightly expand slide on Hilbert system.David A. Madore2023-12-121-2/+13
* A brief word about the S,K,I combinators.David A. Madore2023-12-121-0/+44
* A brief word on Curry-Howard for sequent calculus, and the lambda-bar-calculus.David A. Madore2023-12-121-0/+62
* Sketch of proof of cut elimination, and applications thereof.David A. Madore2023-12-121-6/+91
* Better use of mathpartir.David A. Madore2023-12-121-88/+88
* Examples of cut elimination steps.David A. Madore2023-12-121-15/+76
* Start talking about cut elimination.David A. Madore2023-12-111-0/+79
* Equivalence of sequent calculus with natural deduction.David A. Madore2023-12-111-0/+55
* Sequent calculus: better discuss structural rules.David A. Madore2023-12-111-0/+38
* Make the fix less confusing.David A. Madore2023-12-111-6/+3
* Fix a mistake: contraction rule cannot be dispensed with.David A. Madore2023-12-091-10/+7
* Fix various mistakes noted during lecture on 2023-12-08.David A. Madore2023-12-081-9/+12
* Thinko.David A. Madore2023-12-051-1/+1
* Various minor changes (upon re-reading).David A. Madore2023-12-051-17/+28
* Examples of sequent calculus proofs.David A. Madore2023-12-041-3/+74
* The rules of sequent calculus.David A. Madore2023-12-041-0/+84
* Functoriality of connectors and of logical formulae.David A. Madore2023-12-041-24/+123
* Positive and negative occurrences.David A. Madore2023-12-041-0/+43
* A start of polymorphism, and substitution for type/prop variables.David A. Madore2023-12-041-2/+35
* Comments on negation and double negation.David A. Madore2023-12-041-0/+40
* Curry-Howard: a recapitulation.David A. Madore2023-12-041-4/+47
* Various minor changes or additions.David A. Madore2023-12-041-1/+21
* More discussion of the logical connectors.David A. Madore2023-12-041-4/+53
* Non-uniqueness of proofs.David A. Madore2023-12-031-1/+57
* Various examples of Curry-Howard.David A. Madore2023-12-031-1/+81
* Curry-Howard correspondence for true and false.David A. Madore2023-12-031-1/+32
* An example of Curry-Howard with disjunction.David A. Madore2023-12-031-0/+41
* Remarks on products and sums.David A. Madore2023-12-031-2/+44
* Curry-Howard correspondence for disjunction.David A. Madore2023-12-031-0/+31
* An example of Curry-Howard with implication.David A. Madore2023-12-031-0/+31
* An example of Curry-Howard with conjunction.David A. Madore2023-12-031-4/+74
* Curry-Howard correspondence for implication alone.David A. Madore2023-12-031-0/+44
* Brouwer-Heyting-Kolmogorov interpretation of logical connectives.David A. Madore2023-12-031-1/+28
* A few more important tautologies.David A. Madore2023-12-031-1/+5
* Various informal explanations of constructive math / intuitionism.David A. Madore2023-12-021-0/+142
* Classical logic.David A. Madore2023-12-021-3/+71
* Proof of negation vs reduction ad absurdum.David A. Madore2023-12-021-0/+54
* Examples of non-tautologies.David A. Madore2023-12-021-3/+37
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-22 21:07:11 +0000