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 (
Expand
)
Author
Age
Files
Lines
...
*
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
*
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
[prev]
[next]