Plans for a glossary of terms in the area of programming language theory, type theory and formal methods (PLT, TT, FM)

glossary.md

A

• abstract data type (ADT)
• abstract interpretation
• abstract syntax tree
• α-equivalence (alpha-equivalence)
• algebraic data type (ADT)
• aliasing
• automated reasoning
• axiomatic semantics

B

• β-reduction (beta-reduction)
• big-step semantics
• bootstrapping
• bounded model checking

C

• Calculus of Construction (CoC)
• Calculus of Inductive Constructions (CIC)
• Church encoding
• Church–Rosser property
• Church–Rosser theorem
• closure
• coeffect
• coinduction
• compilation
• completeness
• computational tree logic (CTL)
• computational type theory
• confluence
• constant folding, constant propagation
• constraint solving
• constructivism
• constructor
• continuation
• continuation-passing style (CPS)
• control flow diagram (CFD), control flow graph (CFG)
• conversion
• corecursion
• counterexample-guided abstract refinement (CEGAR)
• CTL*
• cubical type theory
• cumulative type hierarchy
• Curry–Howard correspondence/isomorphism

D

• data constructor
• data flow diagram (DFD), data flow graph (DFG)
• de Bruijn indices
• dead code elimination
• δ-reduction (delta-reduction)
• denotational semantics (Scott–Strachey semantics)
• dependent elimination
• dependent object types (DOT) calculus
• dependent pattern matching
• dependent type
• Dijkstra monad
• domain

E

• effect
• effect handler
• effects system
• elaboration = type elaboration
• elimination
• erasure = type erasure
• η-conversion, η rule (eta-conversion, eta rule)
• evaluation
• exception
• explicit-state model checking
• expression
• expression problem
• extensionality
• extensional type theory

F

• first-order logic
• fixed point
• functional big-step semantics

G

• generalized algebraic data type (GADT)
• Girard's paradox

H

• head normal form (hnf)
• heterogeneous equality
• higher-kinded type
• higher-order function
• higher-order logic
• higher-order unification
• Hoare logic
• Hoare triple
• homoiconicity
• homotopy type theory (HoTT)

I

• impredicativity
• induction
• induction-recursion
• inductive type
• intensional type theory
• intermediate language (IL), intermediate representation (IR)
• introduction
• intuitionism
• ι-reduction (iota-reduction)

J

• just-in-time compilation (JIT)

K

• kind

L

• λ (lambda) calculus
• lambda cube
• lambda lifting
• linear logic
• linear temporal logic
• linear type
• liveness (property)
• locally nameless representation
• lollipop (⊸)

M

• Martin-Löf type theory (MLTT), MLTT{71,72,73,79}
• memory safety
• metacircular evaluator/interpreter
• metalinguistic abstraction
• metaprogramming
• modal logic
• model checking
• Mogensen–Scott encoding
• monad

N

• normal form
• normalization
• normalization by evaluation

O

• observational equality
• observational type theory
• operational semantics

P

• par (⅋) = multiplicative disjunction
• partial order reduction
• pattern matching
• peephole optimization
• π-calculus (pi-calculus)
• Π-type (Pi-type)
• POPLmark challenge
• predicativity
• preservation
• pretty big-step semantics
• probabilistic Hoare logic
• probabilistic model checking
• program slicing
• progress
• proof assistant
• proof by reflection

Q

• quantitative type theory

R

• recursion
• reduction, reduction step
• refinement
• refinement type
• reflection
• register allocation
• relaxed memory
• rewriting system

S

• safety (property)
• satisfiability (SAT)
• satisfiability modulo theories (SMT)
• Scott encoding
• shape analysis
• side effect
• Σ-type (Sigma-type)
• single static assignment (SSA)
• small-step semantics
• soundness
• statement
• strong normalization
• structural recursion
• subject reduction
• subset type
• subtyping
• symbolic execution
• symbolic model checking
• syntax-directed
• syntax tree
• System F + variations (Fω, Fc, F<:)
• System U

T

• tail call
• tail call optimization (TCO)
• type constraint
• tail recursion
• termination
• theorem proving
• totality
• type
• type constructor
• type elaboration
• type erasure
• Type-in-Type
• type inference
• type reconstruction
• type system
• type universe

U

• unification
• unified theory of dependent types (UTT)
• universe

W

• W-type
• weak head normal form (whnf)

Z

• ζ-reduction, ζ rule (zeta-reduction, zeta rule)