teach/inf110-lfi.git - INF110 (logique et fondements de l'informatique)

	Commit message (Collapse)	Author	Age	Files	Lines
*	The rules of first-order logic.	David A. Madore	2023-12-17	1	-0/+121
\|
*	Start talking about first-order logic.	David A. Madore	2023-12-17	1	-2/+111
\|
*	Start a basic set of slides on higher order logic(s).	David A. Madore	2023-12-17	1	-0/+227
\|
*	Give the proof in Coq as well.	David A. Madore	2023-12-16	1	-0/+29
\|
*	More exercises in intiotionistic propositional logic.	David A. Madore	2023-12-16	1	-1/+87
\|
*	Say something about the value restriction.	David A. Madore	2023-12-16	1	-3/+37
\|
*	Briefly mention the problem of let-bound polymorphism.	David A. Madore	2023-12-16	1	-0/+84
\|
*	Summarize properties of Hindley-Milner.	David A. Madore	2023-12-16	1	-0/+46
\|
*	An example of the full H-M algorithm.	David A. Madore	2023-12-16	1	-5/+58
\|
*	Description of the unification phase of Hindley-Milner.	David A. Madore	2023-12-16	1	-1/+35
\|
*	Start describing the Hindley-Milner algorithm.	David A. Madore	2023-12-16	1	-4/+113
\|
*	An exercise involving call/cc.	David A. Madore	2023-12-15	1	-0/+42
\|
*	An exercise on Curry-Howard.	David A. Madore	2023-12-15	1	-0/+109
\|
*	Decide that label strings should be in English.	David A. Madore	2023-12-15	1	-14/+14
\|
*	Note the disjunction property for realizability semantics.	David A. Madore	2023-12-15	1	-1/+8
\|
*	Try to make description of S,K,I combinators slightly less confusing.	David A. Madore	2023-12-15	1	-8/+10
\|
*	Fix typing errors.	David A. Madore	2023-12-15	1	-2/+2
\|
*	Typo.	David A. Madore	2023-12-15	1	-1/+1
\| \| \| \|	(Thanks, Cyrille Deuss.)
*	Barely start writing about Hindley-Milner.	David A. Madore	2023-12-14	1	-0/+42
\|
*	Something about Medvedev's logic of finite problems.	David A. Madore	2023-12-14	1	-0/+68
\|
*	More on propositional realizability.	David A. Madore	2023-12-14	1	-1/+249
\|
*	Examples in open sets semantics.	David A. Madore	2023-12-14	1	-2/+54
\|
*	Semantics of open sets.	David A. Madore	2023-12-14	1	-0/+61
\|
*	More about Kripke frames and semantics.	David A. Madore	2023-12-14	1	-3/+159
\|
*	Truth-table semantics.	David A. Madore	2023-12-14	1	-0/+142
\|
*	General handwaving about semantics in logic.	David A. Madore	2023-12-14	1	-0/+81
\|
*	More remarks about CPS.	David A. Madore	2023-12-14	1	-11/+45
\|
*	Hopefully unfsck the whole situation with CPS translation and typing.	David A. Madore	2023-12-14	1	-45/+135
\|
*	Try to fix CPS transformation, but this is still broken. :-(	David A. Madore	2023-12-13	1	-35/+39
\|
*	Change chapter title to include propositional calculus.	David A. Madore	2023-12-13	1	-1/+1
\|
*	Add a few call/cc puzzles.	David A. Madore	2023-12-13	1	-1/+18
\|
*	Many remarks on continuation-passing-style.	David A. Madore	2023-12-13	1	-1/+86
\|
*	Applications of continuations.	David A. Madore	2023-12-13	1	-2/+33
\|
*	Additional remark.	David A. Madore	2023-12-13	1	-2/+14
\|
*	Systematization of continuation-passing-style.	David A. Madore	2023-12-13	1	-0/+85
\|
*	Expand last example slightly.	David A. Madore	2023-12-12	1	-1/+5
\|
*	Discuss continuation-passing-style.	David A. Madore	2023-12-12	1	-2/+53
\|
*	Typing of call/cc.	David A. Madore	2023-12-12	1	-1/+128
\|
*	A brief description of continuations and call/cc.	David A. Madore	2023-12-12	1	-2/+111
\|
*	Slightly expand slide on Hilbert system.	David A. Madore	2023-12-12	1	-2/+13
\|
*	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
\| \| \| \| \| \|	(See discussion in example 3.1.3 in Troelstra & Schwichtenberg: the system I presented is essentially their G2i, and the contraction rule is necessary.)