Commit message (Collapse) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
* | A (humorous) graphical representation of the Curry-Howard correspondence. | David A. Madore | 2023-11-24 | 3 | -4/+27 | |
| | ||||||
* | Graphical representation of typing rules. | David A. Madore | 2023-11-22 | 1 | -8/+35 | |
| | ||||||
* | Brief summary of Tait's proof of normalization of the STLC. | David A. Madore | 2023-11-22 | 1 | -5/+42 | |
| | ||||||
* | Clarification on how to read a derivation tree. | David A. Madore | 2023-11-22 | 1 | -0/+8 | |
| | ||||||
* | Give some examples of terms and types in the STLC before formalizing. | David A. Madore | 2023-11-22 | 1 | -4/+44 | |
| | ||||||
* | A first taste of the Curry-Howard correspondence. | David A. Madore | 2023-11-22 | 1 | -1/+34 | |
| | ||||||
* | A few clarifications on stability of decidable and semidecidable sets. | David A. Madore | 2023-11-22 | 1 | -3/+7 | |
| | ||||||
* | Exercise on computable inseparability. | David A. Madore | 2023-11-21 | 1 | -0/+129 | |
| | | | | (Taken from INF105 test from 2018-02-06, slightly rewritten.) | |||||
* | Prepare exercise sheet for publication. | David A. Madore | 2023-11-21 | 1 | -19/+23 | |
| | ||||||
* | Exercise on looping Turing machines. | David A. Madore | 2023-11-21 | 1 | -0/+71 | |
| | ||||||
* | Exercise showing that the indices of total functions is not semi-decidable ↵ | David A. Madore | 2023-11-21 | 1 | -0/+140 | |
| | | | | nor co-semi-decidable. | |||||
* | Fix various mistakes (or notational blunders) noted during lecture on ↵ | David A. Madore | 2023-11-20 | 1 | -5/+5 | |
| | | | | 2023-11-20. | |||||
* | The graph of the Ackermann function is p.r. | David A. Madore | 2023-11-20 | 1 | -0/+235 | |
| | ||||||
* | More exercises on computability. | David A. Madore | 2023-11-19 | 1 | -13/+250 | |
| | ||||||
* | Some exercises on computability. | David A. Madore | 2023-11-17 | 1 | -0/+350 | |
| | ||||||
* | Fix various mistakes (or notational blunders) noted during lecture on ↵ | David A. Madore | 2023-11-17 | 1 | -21/+24 | |
| | | | | 2023-11-17. | |||||
* | Beta-reduction and strong normalization (to be continued). | David A. Madore | 2023-11-16 | 1 | -0/+41 | |
| | ||||||
* | More properties of typing, incl. the substitution lemma. | David A. Madore | 2023-11-16 | 1 | -6/+97 | |
| | ||||||
* | Some properties of derivation in simply-typed lambda-calculus. | David A. Madore | 2023-11-16 | 1 | -0/+111 | |
| | ||||||
* | Give an example of a fully written out derivation tree. | David A. Madore | 2023-11-15 | 1 | -0/+39 | |
| | ||||||
* | Rules of the simply-typed lambda-calculus. | David A. Madore | 2023-11-15 | 1 | -3/+122 | |
| | ||||||
* | Various curiosities. | David A. Madore | 2023-11-15 | 1 | -3/+32 | |
| | | | | (Thanks to Thierry Martinez for most of these suggestions.) | |||||
* | Type systems for logic. | David A. Madore | 2023-11-15 | 1 | -1/+67 | |
| | ||||||
* | Curry's paradox (an interlude). | David A. Madore | 2023-11-15 | 1 | -0/+88 | |
| | ||||||
* | Typing and termination. | David A. Madore | 2023-11-15 | 1 | -0/+41 | |
| | ||||||
* | Tasks in a typing system. | David A. Madore | 2023-11-15 | 1 | -1/+45 | |
| | ||||||
* | More examples of languages with interesting type systems. | David A. Madore | 2023-11-15 | 1 | -4/+47 | |
| | ||||||
* | Use of typing systems beyond value control. | David A. Madore | 2023-11-15 | 1 | -0/+36 | |
| | ||||||
* | Minor clarification. | David A. Madore | 2023-11-14 | 1 | -2/+3 | |
| | ||||||
* | Generalities about polymorphism. | David A. Madore | 2023-11-14 | 1 | -14/+64 | |
| | ||||||
* | Basic set of slides on typing. | David A. Madore | 2023-11-14 | 1 | -0/+296 | |
| | ||||||
* | Fix mistakes in numbering of recursive functions. | David A. Madore | 2023-11-08 | 1 | -5/+8 | |
| | | | | (Thanks, "RRt".) | |||||
* | Rephrase for clarity. | David A. Madore | 2023-11-08 | 1 | -2/+2 | |
| | ||||||
* | Typos. | David A. Madore | 2023-11-06 | 1 | -3/+3 | |
| | | | | (Thanks, Ilia.) | |||||
* | Reread up to Rice's theorem. | David A. Madore | 2023-11-04 | 1 | -97/+166 | |
| | ||||||
* | Apparently "francais" is now obsolete. Sigh. | David A. Madore | 2023-11-03 | 1 | -1/+1 | |
| | ||||||
* | Switch to Latin Modern font (and fudge some line breaks). | David A. Madore | 2023-11-03 | 1 | -3/+4 | |
| | ||||||
* | Reformulate formalizations of Turing reduction. | David A. Madore | 2023-11-03 | 1 | -21/+23 | |
| | | | | (Still not happy about this.) | |||||
* | Typo. | David A. Madore | 2023-11-02 | 1 | -1/+1 | |
| | | | | (Thanks, "jeanas".) | |||||
* | One formalization of Turing reduction was wrong: quick fix (to be improved!). | David A. Madore | 2023-11-02 | 1 | -5/+5 | |
| | ||||||
* | A few things about Turing reduction. | David A. Madore | 2023-11-02 | 1 | -3/+128 | |
| | ||||||
* | Many-to-one reduction, and a new proof of Rice's theorem. | David A. Madore | 2023-11-02 | 1 | -1/+160 | |
| | ||||||
* | Rice's theorem. | David A. Madore | 2023-11-02 | 1 | -0/+88 | |
| | | | | Thanks, "jeanas" for the reminder that this is important. | |||||
* | Numbering of recursive functions (compute explicit code for sum function). | David A. Madore | 2023-11-01 | 1 | -4/+14 | |
| | ||||||
* | Minor changes. | David A. Madore | 2023-11-01 | 1 | -4/+4 | |
| | ||||||
* | Googological meditation. | David A. Madore | 2023-11-01 | 1 | -5/+39 | |
| | ||||||
* | Untyped lambda-calculus and a recursive type. | David A. Madore | 2023-11-01 | 1 | -0/+36 | |
| | ||||||
* | Typo. | David A. Madore | 2023-11-01 | 1 | -1/+1 | |
| | | | | (Thanks, Fabrice!) | |||||
* | Various minor corrections and clarifications. | David A. Madore | 2023-10-30 | 1 | -9/+13 | |
| | ||||||
* | Some comments and final thoughts. | David A. Madore | 2023-10-30 | 1 | -11/+109 | |
| |