Ex Libris                        Wanted                           
blank

       
blank

blank
blank
blank
blank
Girard J.-Y., Taylor P., Lafont Y. Proofs and Types
Girard J.-Y., Taylor P., Lafont Y.  Proofs and Types









?
Ctrl+Enter


: Proofs and Types

: Girard J.-Y., Taylor P., Lafont Y.

:

Translated (from French) and developed from notes prepared for a course at the University of Paris VII. Deals with the mathematical background of the application to computer science of aspects of logic (namely the correspondence between propositions and types). Treats both the traditional logic material, and its prospective application to computer science.


: en

: // /

:

ed2k: ed2k stats

: 1989

: 176

: 11.12.2004

: | | ID
blank
$F_0$ (parallel or)      61 70
$\exists$      see Existential quantifier
$\lambda$      see Abstraction
$\lambda$-calculus      12 15
$\lambda$-calculus, Church Rosser property      22
$\lambda$-calculus, conversion      18
$\lambda$-calculus, head normal form      19
$\lambda$-calculus, natural deduction      11 19
$\lambda$-calculus, normalisation      24 42
$\lambda$-calculus, second order polymorphic      82
$\lambda$-calculus, semantics      54 67
$\lambda$-calculus, untyped      19 22 133
$\mathcal{L}$ (left logical rules)      see Sequent calculus
$\mathcal{P}\omega$      see Scott
$\mathcal{R}$ (right logical rules)      see Sequent calculus
$\pi$      see System F
$\pi^1$, $\pi^2$, $\Pi^1$, $\Pi^2$      see Components
$\sum$ (existential type) in F      86 145
$^{\mathcal{L}}$      see Asymmetrical interpretation
$^{\mathcal{R}}$      see Asymmetrical interpretation
(CR 13)      see Reducibility
0 (zero)      see Integers
Abramsky      i 55
Abstraction $(\lambda)$ conversion      13
Abstraction $(\lambda)$ introduction      12 20
Abstraction $(\lambda)$ realisability      127
Abstraction $(\lambda)$ reducibility      45
Abstraction $(\lambda)$ semantics      68 144
Abstraction $(\lambda)$ syntax      15 82
Absurdity $(\bot)$      6 95
Absurdity $(\bot)$, commuting conversion      78
Absurdity $(\bot)$, denotation (f)      see Booleans and undefined object $(\empty)$
Absurdity $(\bot)$, empty type (Emp and $\varepsilon_U$)      80
Absurdity $(\bot)$, linear logic (\bot and 0)      154
Absurdity $(\bot)$, natural deduction (\bot\mathcal{E})      73
Absurdity $(\bot)$, realisability      129
Absurdity $(\bot)$, sequent calculus (\emptyset\vdash\emptyset)      29
Ackermanns function      51
Algebraic domain      56
Alive hypothesis      9
All $(\forall)$      see Universal quantifier
Alternations of quantifiers      58 124
Alternative conjunction (\&)      see Direct product
Amalgamated sum      96 134
Analysis (second order arithmetic)      114
AND      see Conjunction
Application, conversion      13
Application, elimination      12 20
Application, realisability      127
Application, reducibility      43
Application, semantics (App)      69
Application, stability (Berry order)      65
Application, syntax      15 82
Application, trace formula (App)      63 64 144
Approximation of points and domains      57 134
Arrow type      see Implication and function-space
Associativity of sum type      98
Asymmetrical interpretation      34
Atomic formulae      4 5 30 112 160
Atomic points      see Tokens
Atomic sequents      112
Atomic types      15 48
Automated deduction      28 34
Automorphisms      134
Axiom, comprehension      114 118 123
Axiom, excluded middle      6 156
Axiom, hypothesis      10
Axiom, identity      30
Axiom, link      156
Axiom, proper      112
Bad elimination      77
Barendregt      22
Berry      54
Berry order $(\leq _B)$      65 66 135 146
Beta $(\beta)$ rule      see Conversion
Binary completeness      56
Binary trees (Bintree)      93
Binding variables      5 12 15 83 161
Boole      3
Booleans      4
Booleans in F $(\Pi X.X\rightarrow X\rightarrow X)$      84 140
Booleans in system F      84
Booleans in T (Bool, T, F)      48 50 70
Booleans, coherence space, $[\Pi X.X\rightarrow X\rightarrow X]$      140
Booleans, coherence space, Bool      56 60 70
Booleans, commuting conversion      86
Booleans, conversion      48
Booleans, denotation (t and f)      4
Booleans, totality      149
Bounded meet      see Pullback
Boundedly complete domains      140
Brouwer      6
By values      51 70 91 133
C, C?      see Contraction
Camembert      3
CAML      81
Candidate, reducibility      43 115 116
Candidate, totality      58 149
Cantor      1
Cartesian closed category      54 62 67 69 95 152
Cartesian natural transformation      see Berry order
Cartesian product      see Product
Casewise definition (D)      48 83 97
Category      59 95 133 135
Characteristic subgroup      134
Church Rosser property      16 22 49 74 79 90 114 152 159
CLIQUE      57 62 101 138
Closed normal form      19 52 121
Coclosure      135
Coherence space      56
Coherence space, $\Pi$ types      143
Coherence space, booleans, $[\Pi X.X\rightarrow X\rightarrow X]$      140
Coherence space, booleans, Bool      56 60 70
Coherence space, coherence relation $( ^\frown_\smile )$      56
Coherence space, direct product (\&)      62
Coherence space, direct sum $(\oplus)$      96 103
Coherence space, empty type $(\mathcal{E}mp)$      104 139
Coherence space, function space (\rightarrow)      64 102 138
Coherence space, integers $[\Pi X.X\rightarrow X\rightarrow X]$      147
Coherence space, integers flat (Int)      56 60 66 70
Coherence space, integers lazy $(Int^+)$      71 98
Coherence space, linear implication $(\multimap)$      100 104 138
Coherence space, linear negation $(\mathcal{A}^{\bot})$      100 138
Coherence space, of course (!)      101 138 145
Coherence space, Pair, $\Pi^1$, $\Pi^2$      68
Coherence space, partial functions $(\mathcal{PF})$      66
Coherence space, semantics      67 132
Coherence space, singleton (Sgl)      104 139
Coherence space, tensor product $(\oplus)$      104 138
Coherence space, tensor sum or par $(\maltese)$      104
Coherence space, tokens and web      56
Coherent or spectral space      56
Collect (forming trees)      94
Communicating processes      155
Commutativity of logic      29
Commuting conversion of sum      see Conversion
Compact      59 66
Compact-open topology      55
Complementary graph      see Linear negation
Complete subgraph      see Clique
Complexity, algorithmic      53 111 143
Complexity, logical      42 58 114 122 124 140
Components ($\pi^1$ and $\pi^2$), elimination      19
Components ($\pi^1$ and $\pi^2$), reducibility      43
Composition, stable functions      69
Comprehension scheme      114 118 123 126
Computational significance      1 11 17 112 120
Confluent relation      see Church Rosser property
Conjunction      5
Conjunction and product      11 15 19
Conjunction, conj in Bool      50
Conjunction, conversion      13
Conjunction, cut elimination      105
Conjunction, in F: $\Pi X.(U\rightarrow V\rightarrow X)\rightarrow X      84
Conjunction, linear logic      152
Conjunction, natural deduction, $\wedge\mathcal{I}$, $\wedge 1\mathcal{E}$ and $\wedge 2\mathcal{E}$      10
Conjunction, realisability      126
Conjunction, sequent calculus, $\mathcal{L}1\wedge$, $\mathcal{L}2\wedge$ and $\mathcal{R}\wedge$      31
Cons (add to list)      91
Consistency, equational      16 23 152
Consistency, logical (consis)      42 114 124
Constants by vocation      60 66
Constructors      see Data types in F
Continuity      54 59 137
Contraction, $\mathcal{LC}$ and $\mathcal{RC}$      29
Contraction, linear logic (C?)      154
Contractum      18 (see also Redex
Control features of PROLOG      28
Conversion $(\rightsquigarrow)$      18
Conversion $(\rightsquigarrow)$ in F      83 94
Conversion $(\rightsquigarrow)$, $\lambda$-calculus      11 16 18 69
Conversion $(\rightsquigarrow)$, bogus example      75
Conversion $(\rightsquigarrow)$, booleans (D)      48
Conversion $(\rightsquigarrow)$, commuting      74 78 85 97 103
Conversion $(\rightsquigarrow)$, conjunction $(\wedge)$      13
Conversion $(\rightsquigarrow)$, degree      25
Conversion $(\rightsquigarrow)$, denotational equality      69 132
Conversion $(\rightsquigarrow)$, disjunction $(\vee)$      75 97
Conversion $(\rightsquigarrow)$, existential quantifier $(\exists)$      75
Conversion $(\rightsquigarrow)$, implication (\Rightarrow)      13
Conversion $(\rightsquigarrow)$, infinity (\infty)      72
Conversion $(\rightsquigarrow)$, integers (R, It)      48 51
Conversion $(\rightsquigarrow)$, linear logic (proof nets)      158
Conversion $(\rightsquigarrow)$, natural deduction      13 20
Conversion $(\rightsquigarrow)$, reducibility      43 116
Conversion $(\rightsquigarrow)$, rewrite rules      14
Conversion $(\rightsquigarrow)$, second order      94
Coquand      116 133
Correctness criterion for proof nets      158
Correctness criterion for tokens of IT types      139 142
Couple (forming trees)      93
Cumulative conjunction      see Tensor product
Curry Howard isomorphism      5 150
Curry Howard isomorphism, conjunction and product      14
Curry Howard isomorphism, disjunction and sum      80
Curry Howard isomorphism, implication and functions      14
Curry Howard isomorphism, none in sequent calculus      28
Curry Howard isomorphism, second order      94
Cut rule, Cut      30
Cut rule, elimination of      3 105 151 158
Cut rule, linear logic      153 156 158
Cut rule, natural deduction      35 40
Cut rule, not Church Rosser      150
Cut rule, proofs without      33 159
Cut rule, restriction of      112
D, $\mathcal{D}$      see Casewise definition
Data types in F      87 89
Dead hypothesis      9
Deadlock      155
Deduction (natural)      9
Degree $\partial()$, of formula or type      24 109
Degree d(), of cut or redex      24 109
Delin      see Linearisation
Denotation      1
Denotational semantics      14 54 67 95 132
Dereliction (D?)      154
dI-domains      71 98
Direct product (\&), coherence space      61 67
Direct product (\&), linear logic      152
Direct sum $(\oplus)$, coherence space      96 103 146
Direct sum $(\oplus)$, coherence space, example      66
Direct sum $(\oplus)$, linear logic      152
Directed joins      57 59 66
Discharge      9 12 37 73 161
Discrete graph      see Flat domain
Disjunction      5 6 95
Disjunction and sum      81
Disjunction, commuting conversion      78
Disjunction, conversion      75
Disjunction, cut elimination      106
Disjunction, disj in Bool      50
Disjunction, intuitionistic $\mathcal{L}\vee$      32
Disjunction, intuitionistic property      8 33
Disjunction, linear logic ($\oplus$ and $\maltese$)      152
Disjunction, natural deduction $\vee 1\mathcal{I}$, $\vee 2\mathcal{I}$ and $\vee\mathcal{E}$      73
Disjunction, sequent calculus $\mathcal{L}\vee$, $\mathcal{R}1\vee$ and $\mathcal{R}2\vee$      31
Domain theory      56 132
Domain theory, dI-domains      71 98
Domain theory, domain equations      98
Domain theory, Girard versus Scott      54 66 98
Domain theory, L-domains      140
Domain theory, lifted sum      96
Donkey      134
Dynamic      2 14 54
Elimination      8 48
Elimination, $\forall^2\mathcal{E}$      94 125
Elimination, $\vee\mathcal{E}$, $\bot\mathcal{E}$ and $\exists\mathcal{E}$      73
Elimination, $\wedge 1\mathcal{E}$, $\wedge 2\mathcal{E}$, $\Rightarrow\mathcal{E}$ and $\forall\mathcal{E}$      10
Elimination, application and components      19
Elimination, good and bad      77
Elimination, left logical rules      37 40
Elimination, linear logic      161
Elimination, linearity of      99 103
Elimination, R and D in T      48
Embedding-projection pair      133 134
Empty type and absurdity      80
Empty type in F: $Emp = \Pi X. X$      85 139
Empty type, coherence space $(\mathcal{E}mp)$      95 104 139
Empty type, Emp and $\varepsilon_U$      80
Empty type, linear logic ($\bot$ and 0)      154
Empty type, realisability      129
Equalisers      137
Equations between terms and proofs      see Conversion
Espace coherent      56
Eta rule      see Secondary equations
Evaluation      see Application
Event structures      98
Exchange, $\mathcal{L}X$ and $\mathcal{R}X$      29
Exchange, linear logic (X)      153
Existential quantifier      5 6
Existential quantifier, commuting conversion      78
Existential quantifier, conversion      75
Existential quantifier, cut elimination      108
Existential quantifier, intuitionistic property      8 33
Existential quantifier, natural deduction, $\exists\mathcal{I}$ and $\exists\mathcal{E}$      73
Existential quantifier, sequent calculus, $\mathcal{L}\exists$ and $\mathcal{R}\exists$      32
Existential type in F $(\sum,\nabla)$      86 145
Exponential object      see Implication and function-space
Exponential process      see Complexity algorithmic
Expressive power      50 89 155
Extraction      see Universal application
F (Girard Reynolds system), representable functions      120
F (Girard Reynolds system), semantics      132
F (Girard Reynolds system), strong normalisation      42 114
F (Girard Reynolds system), syntax      82
False denotation $(f,\mathcal{F},F)      see Booleans
False proposition $(\bot)$      see Absurdity
feasible      see Complexity algorithmic
Fields of numbers      134
Filtered colimits      59 137
Finite approximation      57 66 132 134
Finite branching tree      27
Finite normalisation      24
Finite points $(\mathcal{A}_{fin})$      57
Finite presentability      66
Finite, sense and denotation      2
Finite, very      59 66
Fixed point      72 95
Flat domain      57 60 66 70 140
For all $(\forall)$      see Universal quantifier
1 2 3
blank
blank
blank
HR
@Mail.ru
       © , 2004-2017
   | Valid HTML 4.01! | Valid CSS!