| 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 |