summaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
* 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
|
* An exercise on a possible representation of pairs in functional programming ↵David A. Madore2023-12-011-5/+146
| | | | languages.
* Another exercise on various "loopy" reductions.David A. Madore2023-12-011-1/+120
|
* Give two examples of natural deduction proofs (written in sequent style).David A. Madore2023-11-301-0/+41
|
* Some exercises on the untyped lambda-calculus.David A. Madore2023-11-301-0/+286
|
* Minor fixes.David A. Madore2023-11-301-3/+3
|
* Much longer explanation of the Y (and also Z) combinator.David A. Madore2023-11-281-5/+139
|
* Highlight discharged hypotheses in natural deduction presentation.David A. Madore2023-11-281-3/+7
|
* Fix various small mistakes or unclear points.David A. Madore2023-11-281-9/+8
|
* 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
|
* Typo.David A. Madore2023-11-281-1/+1
|
* 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-243-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
|
* A few clarifications on stability of decidable and semidecidable sets.David A. Madore2023-11-221-3/+7
|
* Exercise on computable inseparability.David A. Madore2023-11-211-0/+129
| | | | (Taken from INF105 test from 2018-02-06, slightly rewritten.)
* Prepare exercise sheet for publication.David A. Madore2023-11-211-19/+23
|
* Exercise on looping Turing machines.David A. Madore2023-11-211-0/+71
|
* Exercise showing that the indices of total functions is not semi-decidable ↵David A. Madore2023-11-211-0/+140
| | | | nor co-semi-decidable.
* Fix various mistakes (or notational blunders) noted during lecture on ↵David A. Madore2023-11-201-5/+5
| | | | 2023-11-20.
* The graph of the Ackermann function is p.r.David A. Madore2023-11-201-0/+235
|
* More exercises on computability.David A. Madore2023-11-191-13/+250
|
* Some exercises on computability.David A. Madore2023-11-171-0/+350
|
* Fix various mistakes (or notational blunders) noted during lecture on ↵David A. Madore2023-11-171-21/+24
| | | | 2023-11-17.
* 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
|
* Various curiosities.David A. Madore2023-11-151-3/+32
| | | | (Thanks to Thierry Martinez for most of these suggestions.)
* Type systems for logic.David A. Madore2023-11-151-1/+67
|
* Curry's paradox (an interlude).David A. Madore2023-11-151-0/+88
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-23 11:52:46 +0000