summaryrefslogtreecommitdiffstats
path: root/transp-inf110-02-typage.tex
Commit message (Expand)AuthorAgeFilesLines
* Fix a mistake: contraction rule cannot be dispensed with.David A. Madore2023-12-091-10/+7
* Fix various mistakes noted during lecture on 2023-12-08.David A. Madore2023-12-081-9/+12
* Thinko.David A. Madore2023-12-051-1/+1
* Various minor changes (upon re-reading).David A. Madore2023-12-051-17/+28
* Examples of sequent calculus proofs.David A. Madore2023-12-041-3/+74
* The rules of sequent calculus.David A. Madore2023-12-041-0/+84
* Functoriality of connectors and of logical formulae.David A. Madore2023-12-041-24/+123
* Positive and negative occurrences.David A. Madore2023-12-041-0/+43
* A start of polymorphism, and substitution for type/prop variables.David A. Madore2023-12-041-2/+35
* Comments on negation and double negation.David A. Madore2023-12-041-0/+40
* Curry-Howard: a recapitulation.David A. Madore2023-12-041-4/+47
* Various minor changes or additions.David A. Madore2023-12-041-1/+21
* More discussion of the logical connectors.David A. Madore2023-12-041-4/+53
* Non-uniqueness of proofs.David A. Madore2023-12-031-1/+57
* Various examples of Curry-Howard.David A. Madore2023-12-031-1/+81
* Curry-Howard correspondence for true and false.David A. Madore2023-12-031-1/+32
* An example of Curry-Howard with disjunction.David A. Madore2023-12-031-0/+41
* Remarks on products and sums.David A. Madore2023-12-031-2/+44
* Curry-Howard correspondence for disjunction.David A. Madore2023-12-031-0/+31
* An example of Curry-Howard with implication.David A. Madore2023-12-031-0/+31
* An example of Curry-Howard with conjunction.David A. Madore2023-12-031-4/+74
* Curry-Howard correspondence for implication alone.David A. Madore2023-12-031-0/+44
* Brouwer-Heyting-Kolmogorov interpretation of logical connectives.David A. Madore2023-12-031-1/+28
* A few more important tautologies.David A. Madore2023-12-031-1/+5
* Various informal explanations of constructive math / intuitionism.David A. Madore2023-12-021-0/+142
* Classical logic.David A. Madore2023-12-021-3/+71
* Proof of negation vs reduction ad absurdum.David A. Madore2023-12-021-0/+54
* Examples of non-tautologies.David A. Madore2023-12-021-3/+37
* Some important tautologies.David A. Madore2023-12-021-0/+58
* Yet another presentation of natural deduction proofs (flag presentation).David A. Madore2023-12-021-2/+38
* Another presentation of natural deduction proofs.David A. Madore2023-12-021-2/+49
* Give two examples of natural deduction proofs (written in sequent style).David A. Madore2023-11-301-0/+41
* Minor fixes.David A. Madore2023-11-301-3/+3
* Highlight discharged hypotheses in natural deduction presentation.David A. Madore2023-11-281-3/+7
* Alternative notation for multiple lambdas.David A. Madore2023-11-281-2/+3
* Avoid speaking of type "constructors", a word which might cause confusion.David A. Madore2023-11-281-4/+4
* Rules of inuitionistic propositional calculus in natural deduction style.David A. Madore2023-11-271-0/+39
* Syntax of propositional calculus.David A. Madore2023-11-271-2/+39
* Quick overview of intuitionistic propositional calculus.David A. Madore2023-11-271-0/+38
* A (humorous) graphical representation of the Curry-Howard correspondence.David A. Madore2023-11-241-4/+27
* Graphical representation of typing rules.David A. Madore2023-11-221-8/+35
* Brief summary of Tait's proof of normalization of the STLC.David A. Madore2023-11-221-5/+42
* Clarification on how to read a derivation tree.David A. Madore2023-11-221-0/+8
* Give some examples of terms and types in the STLC before formalizing.David A. Madore2023-11-221-4/+44
* A first taste of the Curry-Howard correspondence.David A. Madore2023-11-221-1/+34
* Beta-reduction and strong normalization (to be continued).David A. Madore2023-11-161-0/+41
* More properties of typing, incl. the substitution lemma.David A. Madore2023-11-161-6/+97
* Some properties of derivation in simply-typed lambda-calculus.David A. Madore2023-11-161-0/+111
* Give an example of a fully written out derivation tree.David A. Madore2023-11-151-0/+39
* Rules of the simply-typed lambda-calculus.David A. Madore2023-11-151-3/+122
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-23 03:02:40 +0000