summaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
* 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
|
* Typing and termination.David A. Madore2023-11-151-0/+41
|
* Tasks in a typing system.David A. Madore2023-11-151-1/+45
|
* More examples of languages with interesting type systems.David A. Madore2023-11-151-4/+47
|
* Use of typing systems beyond value control.David A. Madore2023-11-151-0/+36
|
* Minor clarification.David A. Madore2023-11-141-2/+3
|
* Generalities about polymorphism.David A. Madore2023-11-141-14/+64
|
* Basic set of slides on typing.David A. Madore2023-11-141-0/+296
|
* Fix mistakes in numbering of recursive functions.David A. Madore2023-11-081-5/+8
| | | | (Thanks, "RRt".)
* Rephrase for clarity.David A. Madore2023-11-081-2/+2
|
* Typos.David A. Madore2023-11-061-3/+3
| | | | (Thanks, Ilia.)
* Reread up to Rice's theorem.David A. Madore2023-11-041-97/+166
|
* Apparently "francais" is now obsolete. Sigh.David A. Madore2023-11-031-1/+1
|
* Switch to Latin Modern font (and fudge some line breaks).David A. Madore2023-11-031-3/+4
|
* Reformulate formalizations of Turing reduction.David A. Madore2023-11-031-21/+23
| | | | (Still not happy about this.)
* Typo.David A. Madore2023-11-021-1/+1
| | | | (Thanks, "jeanas".)
* One formalization of Turing reduction was wrong: quick fix (to be improved!).David A. Madore2023-11-021-5/+5
|
* A few things about Turing reduction.David A. Madore2023-11-021-3/+128
|
* Many-to-one reduction, and a new proof of Rice's theorem.David A. Madore2023-11-021-1/+160
|
* Rice's theorem.David A. Madore2023-11-021-0/+88
| | | | Thanks, "jeanas" for the reminder that this is important.
* Numbering of recursive functions (compute explicit code for sum function).David A. Madore2023-11-011-4/+14
|
* Minor changes.David A. Madore2023-11-011-4/+4
|
* Googological meditation.David A. Madore2023-11-011-5/+39
|
* Untyped lambda-calculus and a recursive type.David A. Madore2023-11-011-0/+36
|
* Typo.David A. Madore2023-11-011-1/+1
| | | | (Thanks, Fabrice!)
* Various minor corrections and clarifications.David A. Madore2023-10-301-9/+13
|
* Some comments and final thoughts.David A. Madore2023-10-301-11/+109
|
* Equivalence of functions representable in the lambda-calculus and recursive ↵David A. Madore2023-10-301-4/+205
| | | | functions.
* Representation of p.r. functions by terms of the lambda-calculus.David A. Madore2023-10-301-12/+138
|
* Representation of functions by terms of the lambda-calculus.David A. Madore2023-10-301-2/+38
|
* A remark on arity.David A. Madore2023-10-301-0/+53
|