| Commit message (Collapse) | Author | Age | Files | Lines | ||
|---|---|---|---|---|---|---|
| ... | ||||||
| * | 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 | |
| | | ||||||
| * | The rules of sequent calculus. | David A. Madore | 2023-12-04 | 1 | -0/+84 | |
| | | ||||||
| * | Functoriality of connectors and of logical formulae. | David A. Madore | 2023-12-04 | 1 | -24/+123 | |
| | | ||||||
| * | Positive and negative occurrences. | David A. Madore | 2023-12-04 | 1 | -0/+43 | |
| | | ||||||
| * | A start of polymorphism, and substitution for type/prop variables. | David A. Madore | 2023-12-04 | 1 | -2/+35 | |
| | | ||||||
| * | Comments on negation and double negation. | David A. Madore | 2023-12-04 | 1 | -0/+40 | |
| | | ||||||
| * | Curry-Howard: a recapitulation. | David A. Madore | 2023-12-04 | 1 | -4/+47 | |
| | | ||||||
| * | Various minor changes or additions. | David A. Madore | 2023-12-04 | 1 | -1/+21 | |
| | | ||||||
| * | More discussion of the logical connectors. | David A. Madore | 2023-12-04 | 1 | -4/+53 | |
| | | ||||||
| * | Non-uniqueness of proofs. | David A. Madore | 2023-12-03 | 1 | -1/+57 | |
| | | ||||||
| * | Various examples of Curry-Howard. | David A. Madore | 2023-12-03 | 1 | -1/+81 | |
| | | ||||||
| * | Curry-Howard correspondence for true and false. | David A. Madore | 2023-12-03 | 1 | -1/+32 | |
| | | ||||||
| * | An example of Curry-Howard with disjunction. | David A. Madore | 2023-12-03 | 1 | -0/+41 | |
| | | ||||||
| * | Remarks on products and sums. | David A. Madore | 2023-12-03 | 1 | -2/+44 | |
| | | ||||||
| * | Curry-Howard correspondence for disjunction. | David A. Madore | 2023-12-03 | 1 | -0/+31 | |
| | | ||||||
| * | An example of Curry-Howard with implication. | David A. Madore | 2023-12-03 | 1 | -0/+31 | |
| | | ||||||
| * | An example of Curry-Howard with conjunction. | David A. Madore | 2023-12-03 | 1 | -4/+74 | |
| | | ||||||
| * | Curry-Howard correspondence for implication alone. | David A. Madore | 2023-12-03 | 1 | -0/+44 | |
| | | ||||||
| * | Brouwer-Heyting-Kolmogorov interpretation of logical connectives. | David A. Madore | 2023-12-03 | 1 | -1/+28 | |
| | | ||||||
| * | A few more important tautologies. | David A. Madore | 2023-12-03 | 1 | -1/+5 | |
| | | ||||||
| * | Various informal explanations of constructive math / intuitionism. | David A. Madore | 2023-12-02 | 1 | -0/+142 | |
| | | ||||||
| * | Classical logic. | David A. Madore | 2023-12-02 | 1 | -3/+71 | |
| | | ||||||
| * | Proof of negation vs reduction ad absurdum. | David A. Madore | 2023-12-02 | 1 | -0/+54 | |
| | | ||||||
| * | Examples of non-tautologies. | David A. Madore | 2023-12-02 | 1 | -3/+37 | |
| | | ||||||
| * | Some important tautologies. | David A. Madore | 2023-12-02 | 1 | -0/+58 | |
| | | ||||||
 |
index : teach/inf110-lfi.git | |
| INF110 (logique et fondements de l'informatique) | git repository hosting |
| summaryrefslogtreecommitdiffstats |