Project Page
Index
Table of Contents
ImpAlg.Lattices
Partial Orders
Reversed order
Lattices
Lattice properties
Bounded Lattices
Complete lattices
Tactics
Properties of meet_set and join_set
ImpAlg.Powerset
ImpAlg.HeytingAlgebras
Heyting Algebras
Properties of (complete) Heyting algebras
Implicative Structures
ImpAlg.BooleanAlgebras
Boolean Algebras
Properties of (complete) Boolean algebras
Implicative structures
Properties of the induced IS
Induced implicative algebra
ImpAlg.ImplicativeStructures
Implicative Structures
Definition
Properties of implicative structures
Encoding the λ-calculus
Application
Abstraction
Properties of closures
ImpAlg.OCA
Ordered Combinatory Algebras
Induced implicative structure
ImpAlg.Lambda
λc-calculus in localy nameless representation
Terms
Types
Type system
Instanciation of tactics
Infrastructures
ß-reduction
Substitution for names
ImpAlg.Adequacy
Proof tactics
Embedding of λ-terms and types into implicative structures
Translation of terms
Adequacy wrt ß-reduction
Translation of types
Adequacy
ImpAlg.Combinators
Combinators
I (λx.x)
K (λxy.x)
S (λxyz.xy(zy)
S K K ≤ I
W (λxy.xyy)
λxy.xy
B (λxyz . x(yz))
Combinatory terms
ImpAlg.ImplicativeAlgebras
Implicative Algebras
Properties
Entailment
ImpAlg.Dummies
Dummy Structures
a ↦ b := b
a ↦ b := b
Counter example to ⊢t:A →
t
=
A
ImpAlg.AKS
Abstract Krivine Structures
Induced implicative structure.
Properties of the combinators
Induced implicative algebra