index
:
teach/inf110-lfi.git
master
INF110 (logique et fondements de l'informatique)
git repository hosting
summary
refs
log
tree
commit
diff
stats
log msg
author
committer
range
path:
root
/
transp-inf110-02-typage.tex
Commit message (
Collapse
)
Author
Age
Files
Lines
*
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
|
*
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