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

	Commit message (Collapse)	Author	Age	Files	Lines
...
*	The rules of sequent calculus.	David A. Madore	2023-12-04	1	-0/+84
\|
*	Functoriality of connectors and of logical formulae.	David A. Madore	2023-12-04	1	-24/+123
\|
*	Positive and negative occurrences.	David A. Madore	2023-12-04	1	-0/+43
\|
*	A start of polymorphism, and substitution for type/prop variables.	David A. Madore	2023-12-04	1	-2/+35
\|
*	Comments on negation and double negation.	David A. Madore	2023-12-04	1	-0/+40
\|
*	Curry-Howard: a recapitulation.	David A. Madore	2023-12-04	1	-4/+47
\|
*	Various minor changes or additions.	David A. Madore	2023-12-04	1	-1/+21
\|
*	More discussion of the logical connectors.	David A. Madore	2023-12-04	1	-4/+53
\|
*	Non-uniqueness of proofs.	David A. Madore	2023-12-03	1	-1/+57
\|
*	Various examples of Curry-Howard.	David A. Madore	2023-12-03	1	-1/+81
\|
*	Curry-Howard correspondence for true and false.	David A. Madore	2023-12-03	1	-1/+32
\|
*	An example of Curry-Howard with disjunction.	David A. Madore	2023-12-03	1	-0/+41
\|
*	Remarks on products and sums.	David A. Madore	2023-12-03	1	-2/+44
\|
*	Curry-Howard correspondence for disjunction.	David A. Madore	2023-12-03	1	-0/+31
\|
*	An example of Curry-Howard with implication.	David A. Madore	2023-12-03	1	-0/+31
\|
*	An example of Curry-Howard with conjunction.	David A. Madore	2023-12-03	1	-4/+74
\|
*	Curry-Howard correspondence for implication alone.	David A. Madore	2023-12-03	1	-0/+44
\|
*	Brouwer-Heyting-Kolmogorov interpretation of logical connectives.	David A. Madore	2023-12-03	1	-1/+28
\|
*	A few more important tautologies.	David A. Madore	2023-12-03	1	-1/+5
\|
*	Various informal explanations of constructive math / intuitionism.	David A. Madore	2023-12-02	1	-0/+142
\|
*	Classical logic.	David A. Madore	2023-12-02	1	-3/+71
\|
*	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
\|