summaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* A simple exercise on Kripke semantics.David A. Madore2024-01-041-1/+79
|
* Exercise on comparison of double-negation elimination and excluded middle.David A. Madore2023-12-281-0/+243
|
* Forgotten braces.David A. Madore2023-12-281-2/+2
|
* Fix a number of typos / thinkos / notational blunders in an exercise.David A. Madore2023-12-281-4/+4
|
* Fix various mistakes and make some improvements noted during lecture on ↵David A. Madore2023-12-202-63/+85
| | | | 2023-12-19.
* Change my mind about name of third part.David A. Madore2023-12-191-1/+1
|
* Say something about existentials versus sum types.David A. Madore2023-12-191-0/+42
|
* Add a slide on impredicativity.David A. Madore2023-12-191-0/+52
|
* Slight clarification.David A. Madore2023-12-181-3/+4
|
* The problem of the inhabitedness of the domain.David A. Madore2023-12-181-6/+57
|
* Example proof in first-order logic.David A. Madore2023-12-181-8/+86
|
* The rules of first-order logic.David A. Madore2023-12-171-0/+121
|
* Start talking about first-order logic.David A. Madore2023-12-171-2/+111
|
* Start a basic set of slides on higher order logic(s).David A. Madore2023-12-171-0/+227
|
* Give the proof in Coq as well.David A. Madore2023-12-161-0/+29
|
* More exercises in intiotionistic propositional logic.David A. Madore2023-12-161-1/+87
|
* Say something about the value restriction.David A. Madore2023-12-161-3/+37
|
* Briefly mention the problem of let-bound polymorphism.David A. Madore2023-12-161-0/+84
|
* Summarize properties of Hindley-Milner.David A. Madore2023-12-161-0/+46
|
* An example of the full H-M algorithm.David A. Madore2023-12-161-5/+58
|
* Description of the unification phase of Hindley-Milner.David A. Madore2023-12-161-1/+35
|
* Start describing the Hindley-Milner algorithm.David A. Madore2023-12-161-4/+113
|
* An exercise involving call/cc.David A. Madore2023-12-151-0/+42
|
* An exercise on Curry-Howard.David A. Madore2023-12-151-0/+109
|
* Decide that label strings should be in English.David A. Madore2023-12-151-14/+14
|
* Note the disjunction property for realizability semantics.David A. Madore2023-12-151-1/+8
|
* Try to make description of S,K,I combinators slightly less confusing.David A. Madore2023-12-151-8/+10
|
* Fix typing errors.David A. Madore2023-12-151-2/+2
|
* Typo.David A. Madore2023-12-151-1/+1
| | | | (Thanks, Cyrille Deuss.)
* Barely start writing about Hindley-Milner.David A. Madore2023-12-141-0/+42
|
* Something about Medvedev's logic of finite problems.David A. Madore2023-12-141-0/+68
|
* More on propositional realizability.David A. Madore2023-12-141-1/+249
|
* Examples in open sets semantics.David A. Madore2023-12-141-2/+54
|
* Semantics of open sets.David A. Madore2023-12-141-0/+61
|
* More about Kripke frames and semantics.David A. Madore2023-12-141-3/+159
|
* Truth-table semantics.David A. Madore2023-12-141-0/+142
|
* General handwaving about semantics in logic.David A. Madore2023-12-141-0/+81
|
* More remarks about CPS.David A. Madore2023-12-141-11/+45
|
* 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
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-24 00:37:01 +0000