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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Proof of negation vs reduction ad absurdum.	David A. Madore	2023-12-02	1	-0/+54
\|
*	Examples of non-tautologies.	David A. Madore	2023-12-02	1	-3/+37
\|
*	Some important tautologies.	David A. Madore	2023-12-02	1	-0/+58
\|
*	Yet another presentation of natural deduction proofs (flag presentation).	David A. Madore	2023-12-02	1	-2/+38
\|
*	Another presentation of natural deduction proofs.	David A. Madore	2023-12-02	1	-2/+49
\|
*	Give two examples of natural deduction proofs (written in sequent style).	David A. Madore	2023-11-30	1	-0/+41
\|
*	Minor fixes.	David A. Madore	2023-11-30	1	-3/+3
\|
*	Highlight discharged hypotheses in natural deduction presentation.	David A. Madore	2023-11-28	1	-3/+7
\|
*	Alternative notation for multiple lambdas.	David A. Madore	2023-11-28	1	-2/+3
\|
*	Avoid speaking of type "constructors", a word which might cause confusion.	David A. Madore	2023-11-28	1	-4/+4
\|
*	Rules of inuitionistic propositional calculus in natural deduction style.	David A. Madore	2023-11-27	1	-0/+39
\|
*	Syntax of propositional calculus.	David A. Madore	2023-11-27	1	-2/+39
\|
*	Quick overview of intuitionistic propositional calculus.	David A. Madore	2023-11-27	1	-0/+38
\|
*	A (humorous) graphical representation of the Curry-Howard correspondence.	David A. Madore	2023-11-24	1	-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
\|
*	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