| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | Typo. | David A. Madore | 2024-01-22 | 1 | -1/+1 |
| | | |||||
| * | Adjust TeX sources to make compilation as handout with beamerarticle easier. | David A. Madore | 2024-01-20 | 1 | -6/+15 |
| | | |||||
| * | Forgotten braces. | David A. Madore | 2023-12-28 | 1 | -2/+2 |
| | | |||||
| * | Fix various mistakes and make some improvements noted during lecture on ↵ | David A. Madore | 2023-12-20 | 1 | -30/+52 |
| | | | | | 2023-12-19. | ||||
| * | Say something about the value restriction. | David A. Madore | 2023-12-16 | 1 | -3/+37 |
| | | |||||
| * | Briefly mention the problem of let-bound polymorphism. | David A. Madore | 2023-12-16 | 1 | -0/+84 |
| | | |||||
| * | Summarize properties of Hindley-Milner. | David A. Madore | 2023-12-16 | 1 | -0/+46 |
| | | |||||
| * | An example of the full H-M algorithm. | David A. Madore | 2023-12-16 | 1 | -5/+58 |
| | | |||||
| * | Description of the unification phase of Hindley-Milner. | David A. Madore | 2023-12-16 | 1 | -1/+35 |
| | | |||||
| * | Start describing the Hindley-Milner algorithm. | David A. Madore | 2023-12-16 | 1 | -4/+113 |
| | | |||||
| * | Note the disjunction property for realizability semantics. | David A. Madore | 2023-12-15 | 1 | -1/+8 |
| | | |||||
| * | Try to make description of S,K,I combinators slightly less confusing. | David A. Madore | 2023-12-15 | 1 | -8/+10 |
| | | |||||
| * | Fix typing errors. | David A. Madore | 2023-12-15 | 1 | -2/+2 |
| | | |||||
| * | Typo. | David A. Madore | 2023-12-15 | 1 | -1/+1 |
| | | | | | (Thanks, Cyrille Deuss.) | ||||
| * | Barely start writing about Hindley-Milner. | David A. Madore | 2023-12-14 | 1 | -0/+42 |
| | | |||||
| * | Something about Medvedev's logic of finite problems. | David A. Madore | 2023-12-14 | 1 | -0/+68 |
| | | |||||
| * | More on propositional realizability. | David A. Madore | 2023-12-14 | 1 | -1/+249 |
| | | |||||
| * | Examples in open sets semantics. | David A. Madore | 2023-12-14 | 1 | -2/+54 |
| | | |||||
| * | Semantics of open sets. | David A. Madore | 2023-12-14 | 1 | -0/+61 |
| | | |||||
| * | More about Kripke frames and semantics. | David A. Madore | 2023-12-14 | 1 | -3/+159 |
| | | |||||
| * | Truth-table semantics. | David A. Madore | 2023-12-14 | 1 | -0/+142 |
| | | |||||
| * | General handwaving about semantics in logic. | David A. Madore | 2023-12-14 | 1 | -0/+81 |
| | | |||||
| * | More remarks about CPS. | David A. Madore | 2023-12-14 | 1 | -11/+45 |
| | | |||||
| * | Hopefully unfsck the whole situation with CPS translation and typing. | David A. Madore | 2023-12-14 | 1 | -45/+135 |
| | | |||||
| * | Try to fix CPS transformation, but this is still broken. :-( | David A. Madore | 2023-12-13 | 1 | -35/+39 |
| | | |||||
| * | Change chapter title to include propositional calculus. | David A. Madore | 2023-12-13 | 1 | -1/+1 |
| | | |||||
| * | Add a few call/cc puzzles. | David A. Madore | 2023-12-13 | 1 | -1/+18 |
| | | |||||
| * | Many remarks on continuation-passing-style. | David A. Madore | 2023-12-13 | 1 | -1/+86 |
| | | |||||
| * | Applications of continuations. | David A. Madore | 2023-12-13 | 1 | -2/+33 |
| | | |||||
| * | Additional remark. | David A. Madore | 2023-12-13 | 1 | -2/+14 |
| | | |||||
| * | Systematization of continuation-passing-style. | David A. Madore | 2023-12-13 | 1 | -0/+85 |
| | | |||||
| * | Expand last example slightly. | David A. Madore | 2023-12-12 | 1 | -1/+5 |
| | | |||||
| * | Discuss continuation-passing-style. | David A. Madore | 2023-12-12 | 1 | -2/+53 |
| | | |||||
| * | Typing of call/cc. | David A. Madore | 2023-12-12 | 1 | -1/+128 |
| | | |||||
| * | A brief description of continuations and call/cc. | David A. Madore | 2023-12-12 | 1 | -2/+111 |
| | | |||||
| * | Slightly expand slide on Hilbert system. | David A. Madore | 2023-12-12 | 1 | -2/+13 |
| | | |||||
| * | A brief word about the S,K,I combinators. | David A. Madore | 2023-12-12 | 1 | -0/+44 |
| | | |||||
| * | A brief word on Curry-Howard for sequent calculus, and the lambda-bar-calculus. | David A. Madore | 2023-12-12 | 1 | -0/+62 |
| | | |||||
| * | Sketch of proof of cut elimination, and applications thereof. | David A. Madore | 2023-12-12 | 1 | -6/+91 |
| | | |||||
| * | Better use of mathpartir. | David A. Madore | 2023-12-12 | 1 | -88/+88 |
| | | |||||
| * | Examples of cut elimination steps. | David A. Madore | 2023-12-12 | 1 | -15/+76 |
| | | |||||
| * | Start talking about cut elimination. | David A. Madore | 2023-12-11 | 1 | -0/+79 |
| | | |||||
| * | Equivalence of sequent calculus with natural deduction. | David A. Madore | 2023-12-11 | 1 | -0/+55 |
| | | |||||
| * | Sequent calculus: better discuss structural rules. | David A. Madore | 2023-12-11 | 1 | -0/+38 |
| | | |||||
| * | Make the fix less confusing. | David A. Madore | 2023-12-11 | 1 | -6/+3 |
| | | |||||
| * | Fix a mistake: contraction rule cannot be dispensed with. | David A. Madore | 2023-12-09 | 1 | -10/+7 |
| | | | | | | | (See discussion in example 3.1.3 in Troelstra & Schwichtenberg: the system I presented is essentially their G2i, and the contraction rule is necessary.) | ||||
| * | Fix various mistakes noted during lecture on 2023-12-08. | David A. Madore | 2023-12-08 | 1 | -9/+12 |
| | | |||||
| * | Thinko. | David A. Madore | 2023-12-05 | 1 | -1/+1 |
| | | |||||
| * | Various minor changes (upon re-reading). | David A. Madore | 2023-12-05 | 1 | -17/+28 |
| | | |||||
| * | Examples of sequent calculus proofs. | David A. Madore | 2023-12-04 | 1 | -3/+74 |
| | | |||||
 |
index : teach/inf110-lfi.git | |
| INF110 (logique et fondements de l'informatique) | git repository hosting |
| summaryrefslogtreecommitdiffstats |