| Commit message (Collapse) | Author | Age | Files | Lines | ||
|---|---|---|---|---|---|---|
| ... | ||||||
| * | Start a basic set of slides on higher order logic(s). | David A. Madore | 2023-12-17 | 1 | -0/+227 | |
| | | ||||||
| * | Give the proof in Coq as well. | David A. Madore | 2023-12-16 | 1 | -0/+29 | |
| | | ||||||
| * | More exercises in intiotionistic propositional logic. | David A. Madore | 2023-12-16 | 1 | -1/+87 | |
| | | ||||||
| * | 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 | |
| | | ||||||
| * | An exercise involving call/cc. | David A. Madore | 2023-12-15 | 1 | -0/+42 | |
| | | ||||||
| * | An exercise on Curry-Howard. | David A. Madore | 2023-12-15 | 1 | -0/+109 | |
| | | ||||||
| * | Decide that label strings should be in English. | David A. Madore | 2023-12-15 | 1 | -14/+14 | |
| | | ||||||
| * | 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 | |
| | | ||||||
 |
index : teach/inf110-lfi.git | |
| INF110 (logique et fondements de l'informatique) | git repository hosting |
| summaryrefslogtreecommitdiffstats |