Category:Lambda calculus

• Lambda calculus

A

• Anonymous function
• Applicative computing systems
• Apply

B

• B, C, K, W system
• Beta normal form
• Böhm tree

C

• Calculus of constructions
• Call-by-push-value
• Cartesian closed category
• Church encoding
• Church–Rosser theorem
• Combinatory logic
• Currying

D

• De Bruijn index
• De Bruijn notation
• Director string
• Divergence (computer science)

E

• Explicit substitution

F

• Fixed-point combinator

H

• Higher-order function
• Hindley–Milner type system

I

• Intersection type discipline

K

• Kleene–Rosser paradox
• Knights of the Lambda Calculus
• Krivine machine

L

• Lambda calculus definition
• Lambda cube
• Lambda lifting
• Lambda-mu calculus
• Let expression

M

• Mogensen–Scott encoding
• Montague grammar

N

• Normal form (abstract rewriting)
• Normalisation by evaluation

P

• Pattern calculus
• Pure type system

R

• Reduction strategy
• Rho calculus

S

• Scott–Curry theorem
• Simply typed lambda calculus
• SKI combinator calculus
• Supercombinator
• System F
• System U

T

• Type inhabitation
• Typed lambda calculus

U

• Untyped lambda calculus

Η

• Η-conversion