| Commit message (Expand) | Author | Age | Files | Lines |
... | |
* | 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 |
* | 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 |
* | Yet another presentation of natural deduction proofs (flag presentation). | David A. Madore | 2023-12-02 | 1 | -2/+38 |
* | Another presentation of natural deduction proofs. | David A. Madore | 2023-12-02 | 1 | -2/+49 |
* | An exercise on a possible representation of pairs in functional programming l... | David A. Madore | 2023-12-01 | 1 | -5/+146 |
* | Another exercise on various "loopy" reductions. | David A. Madore | 2023-12-01 | 1 | -1/+120 |
* | Give two examples of natural deduction proofs (written in sequent style). | David A. Madore | 2023-11-30 | 1 | -0/+41 |
* | Some exercises on the untyped lambda-calculus. | David A. Madore | 2023-11-30 | 1 | -0/+286 |
* | Minor fixes. | David A. Madore | 2023-11-30 | 1 | -3/+3 |
* | Much longer explanation of the Y (and also Z) combinator. | David A. Madore | 2023-11-28 | 1 | -5/+139 |
* | Highlight discharged hypotheses in natural deduction presentation. | David A. Madore | 2023-11-28 | 1 | -3/+7 |
* | Fix various small mistakes or unclear points. | David A. Madore | 2023-11-28 | 1 | -9/+8 |
* | Alternative notation for multiple lambdas. | David A. Madore | 2023-11-28 | 1 | -2/+3 |
* | Avoid speaking of type "constructors", a word which might cause confusion. | David A. Madore | 2023-11-28 | 1 | -4/+4 |