Concepts
Key terms and definitions from programming language theory.
A38
Abstract binding graphjust nowAn extension of Abstract binding tree (ABT)s to a Directed acyclic graph (DAG) structure while preserving the binding discipline.Abstract binding tree abtjust nowAn enriched Abstract syntax tree (AST) with bindings and scopes. According to Practical foundations for programming languages , each node in an ABT is either a Variable or an Operator whose arguments are Abstractors.Abstract binding tree abt valence abstractorjust nowAn enriched Abstract syntax tree (AST) with bindings and scopes. According to Practical foundations for programming languages , each node in an ABT is either a Variable or an Operator whose arguments are Abstractors.Abstract data typejust nowA type defined by its operations and their specifications rather than its implementation, providing encapsulation by hiding internal representation while exposing a public interface.Abstract machinejust nowA formal model of computation defined by a set of states, an initial state, final states, and a Transition function specifying how states evolve step-by-step until halting.Abstract syntax tree astjust now(Syntax & Grammar) According to Practical foundations for programming languages , a tree representation of a term's essential structure (not necessarily a program), omitting superficial syntactic details like parentheses, delimiters, and keywords. Can be of some specified Sorts.Abstract syntax tree ast labeled treejust now(Syntax & Grammar) According to Practical foundations for programming languages , a tree representation of a term's essential structure (not necessarily a program), omitting superficial syntactic details like parentheses, delimiters, and keywords. Can be of some specified Sorts.Abstractorjust now$x 1,\dots, x n.a$ -> Within $a$, we can additionally use $x 1,\dots, x n$.Actual parameter argumentjust now(Syntax & Grammar) According to Practical foundations for programming languages , the child of an Operator in an Abstract syntax tree (AST).Admissibilityjust nowNo description yetAdmissibility judgmentjust nowNo description yetAdmissiblejust nowNo description yetAlgebraic data typejust nowA composite type formed by combining Sum types (variants/tagged unions) and product types (tuples/records), enabling precise modeling of data structures like Option, Result, or tree nodes. Synonymous with Sum of products (SoP).Aliasingjust nowA semantic phenomenon where multiple identifiers, references, or paths denote the same memory location, causing mutations through one to be observable through the others - complicating reasoning, optimization, and safety guarantees.Alpha conversion renamingjust nowExample:Alpha conversion renaming variable capture capture avoidingjust nowExample:Alpha equivalencejust nowThen, $= \\alpha$ is the strongest Congruence on $\\mathcal{A}$that contains the followings:Alpha variantjust nowIf two terms are related by the Alpha-equivalence relation, they are alpha-variants.Antecedentjust nowThe part above the line in a typing rule - the Premises that must hold before the Conclusion can be drawn (\"if\" part).Antisymmetricjust nowA property of a Binary relation $R$ such that if $t\ R\ s$ and $s\ R\ t$ then $s = t$, for every $t$, $s$ $\in T$.Antisymmetryjust nowNo description yetApi boundaryjust nowNo description yetApplication function calljust nowThe fundamental operation of applying a function to an argument.Architecture invariantjust nowNo description yetArityjust now(Syntax & Grammar) According to Practical foundations for programming languages , a syntactic type signature of an Operator, determining the Sort of an operator and the number and the sorts of the arguments expected by the operator.Arrow typejust nowThis generalization unifies simple function types, universal types ($\\forall\\alpha.T$), and dependent function types under a single constructor.Assertionjust nowSynonymous with Judgment.Associativityjust nowA parsing rule that determines grouping when the same operator repeats (left: a - b - c = (a - b) - c; right: a :: b :: c = a :: (b :: c)).Assume guarantee reasoningjust nowA pattern where interacting components have mutual obligations - one component assumes what another guarantees, and vice versa (e.g., lambda assumes parameter has type $T$, application guarantees it;Ast rewritingjust nowA program transformation technique that modifies the Abstract syntax tree (AST) to implement features like Macros, optimizations, or language extensions before code generation.Autoboxingjust nowExample:Automated theorem proverjust nowA tool that attempts to prove theorems automatically without human guidance, using techniques like resolution, rewriting, or SAT/SMT solving (contrast with interactive provers like Coq that require uAutomated theorem prover sat solver smt solverjust nowA tool that attempts to prove theorems automatically without human guidance, using techniques like resolution, rewriting, or SAT/SMT solving (contrast with interactive provers like Coq that require uAutomatic memory managementjust nowA language or runtime mechanism that handles allocation and deallocation of memory without explicit programmer intervention - encompassing techniques like Garbage collection, reference counting, and ownership systems.Axiomjust nowA Rule with no Premise.Axiom inference rulejust nowAn Axiom is an Inference rule with no premise.Axiom rule proper rulejust nowAn Axiom is an Inference rule with no premise.Axiomatic semanticsjust nowA style of semantics that defines a language based on its proof rules/laws, rather than how it runs or what mathematical objects it denotes.B25
Backward chainingjust nowA proof technique for Judgments that starts from the desired judgement and works backwards towards the Axioms.Backward chaining searchjust nowA search strategy for a Derivation of some Judgment that starts from the desired Judgment as the initial goal, picks a rule at each step with the conclusion as the current goal, adds its premises as subgoals into a queue & continues until all subgoals are Axioms.Backward chaining search backward chainingjust nowA search strategy for a Derivation of some Judgment that starts from the desired Judgment as the initial goal, picks a rule at each step with the conclusion as the current goal, adds its premises as subgoals into a queue & continues until all subgoals are Axioms.Backward chaining search goal directedjust nowA search strategy for a Derivation of some Judgment that starts from the desired Judgment as the initial goal, picks a rule at each step with the conclusion as the current goal, adds its premises as subgoals into a queue & continues until all subgoals are Axioms.Basic judgmentjust nowNo description yetBehavioral observational contextual equivalencejust nowExample: $\lambda x.\ x \simeq \lambda x.\ (\lambda y.\ y)\ x$Beta equivalencejust nowA Binary relation that relates terms connected by Beta-reduction - $(\lambda x.\ t)\ s = \beta [x\to s]t$ - capturing the fundamental computation rule of function application.Beta redex reducible expressionjust nowA term of the form: $t 1\ t 2$, in which $t 1$ is a Lambda abstraction and $t 2$ is any term.Beta reductionjust nowThe act of reducing a Beta-redex/Reducible expression by substituting the redex's argument into its function body.Beta reduction beta redex reducible expressionjust nowThe act of reducing a Beta-redex/Reducible expression by substituting the redex's argument into its function body.Big step natural operational semanticsjust nowA style of semantic which defines evaluation via Evaluation statement/judgement of the form $t \\Downarrow v$, relating a term directly to its final value in a single derivation rather than through intBig step natural operational semantics small stepjust nowA style of semantic which defines evaluation via Evaluation statement/judgement of the form $t \\Downarrow v$, relating a term directly to its final value in a single derivation rather than through intBinary relationjust nowAn N-place relation where $n = 2$.Binderjust nowA syntactic construct that introduces a variable and defines its scope. In Lambda calculus, it's the variable directly following $\lambda$.Bindingjust nowAn association between a name and an entity (value, location, type, function, etc.) within a given scope.Binding structure of syntaxjust nowA generalization of Abstract binding tree (ABT).Blame trackingjust nowA mechanism that identifies which party (module, component, contract boundary) is responsible when a Contract violation occurs.Blockjust nowA syntactic construct that groups statements and typically introduces a new scope for local bindings - delimited by braces { }, keywords (begin/end), or indentation depending on the language.Bnfjust nowA Metalanguage notation for specifying Context-free grammars, using production rules of the form $\text{<nonterminal>} ::= \text{expression}$ to define the syntax of formal languages.Boolean blindnessjust nowf = if isZero n then y else f (pred n)Borrow checkerjust nowNo description yetBottom up constructionjust nowSynonymous with Forward chaining.Bound variablejust nowA variable bound by an enclosing $\lambda$.Branch coveragejust nowA testing metric requiring that every branch (true/false of each conditional) is executed at least once - difficult to achieve in testing but automatic in type checking since type checkers traverse boBrouwer heyting kolmogorov bhk interpretationjust nowMotivation. Classical logic tells you that something exists, not how to find it. BHK says to prove something exists, you must exhibit a Witness.C64
Calculus of inductive constructionjust nowTools: Rocq (formerly Coq)Call by namejust now(Lambda calculus, Semantics) An evaluation strategy that is Normal order but Beta-reduction inside Lambda abstraction is not allowed.Call by needjust now(Lambda calculus, Semantics, Pure lambda calculus) An evaluation strategy similar to Call by name, but terms' values are cached to avoid re-evaluation.Call by need call by name call by value normal order fulljust now(Lambda calculus, Semantics, Pure lambda calculus) An evaluation strategy similar to Call by name, but terms' values are cached to avoid re-evaluation.Call by valuejust now(Lambda calculus, Semantics) A Strict/Eager evaluation strategy in which Beta-redex/Reducible expressions inside lambda abstractions must not be reduced.Capture avoiding substitutionjust nowRules in Pure/Untyped lambda calculus:Capture avoiding substitution variable capturejust nowRules in Pure/Untyped lambda calculus:Cascading sequential letjust now(let ([x 1]Chomsky hierarchyjust nowA classification of formal grammars by expressiveness - from simplest to most powerful: regular, Context-free (parsers), Context-sensitive (type systems), recursively enumerable; explains why parsingChurch booleanjust nowEncoding:Church numeraljust nowTools: Rocq (formerly Coq)Church numeral rocqjust nowChurch's encoding of numbers used in Pure/Untyped lambda calculus.Circular dependencyjust nowNo description yetClassjust nowA blueprint or template that defines the structure (fields) and behavior (methods) for creating objects, serving as a factory for instantiating objects with shared characteristics.Class extensionjust now(Java) The { ... } part in class Sub extends Sup { ... }, can be conceptually viewed as a Mixin specifically applied to Sup.Class patternjust nowThis pattern has many variants:Closed recursionjust nowWhen utilizing the Class pattern to define classes with method calls referencing other methods, a recursion pattern that causes method reference to be resolved immediately right at class definition.Closed termjust nowA Lambda term with no Free variable.Closed underjust nowNo description yetClosurejust now(Language feature/design, Semantics) A function value that remembers its surrounding Environment.Code semantic modeljust nowNo description yetCodomainjust nowA property of a function specifying the set of values it produces as outputs.Combinatorjust nowA Lambda term that contains no Free variable, or in other words, a Closed term.Commandjust now[Rocq] A top-level directive in Rocq that controls the environment (like `Definition`, `Theorem`, `Print`, `Check`) rather than operating within a proof.Command patternjust nowNo description yetCompilation unitjust nowNo description yetCompilerjust nowMathematically, denote $\\mathcal{P} S$ as the set of programs in the source language and $\\mathcal{P} T$ as the set of programs in the target language. Then, a compiler is a function $C: \\mathcal{P} S \\to \\mathcal{P} T$Compiler interpreterjust nowNo description yetCompletejust nowThe adjective form of Completeness.Completenessjust nowNo description yetComputabilityjust nowThe property of a mathematical problem that can be solved by a program.Computation rulejust nowA rule performing an actual reduction step (e.g., Beta-reduction), as opposed to Congruence rule which merely propagate evaluation into subterms.Computation rule congruence rulejust nowA rule performing an actual reduction step (e.g., Beta-reduction), as opposed to Congruence rule which merely propagate evaluation into subterms.Computation theoryjust nowThe branch of theoretical computer science studying what can be computed and with what resources - includes models of computation (Turing machines, Lambda calculus), Decidability (halting problem, RicConclusionjust nowThe consequent Judgment of an Inference rule that is derived when all its Premises are satisfied.Concolic testingjust nowA testing technique combining concrete execution with symbolic reasoning - runs program with real values while simultaneously tracking symbolic constraints, then solves constraints to generate inputsConcrete generator stylejust nowA style of formal definition that defines a set as a union of a sequence $S 0 \\subseteq S 1 \\subseteq \\dots$ where each $S {i+1}$ is built from $S i$ using rules - e.g., for naturals: $S 0 = \\emptyset$Concrete rulejust nowA specific instance of a Rule schema where all Metavariables are replaced with actual terms - the schema is the general pattern, the concrete rule is a particular instantiation.Concrete surface syntaxjust nowThe textual representation programmers actually write, including parentheses, keywords, and punctuation - as opposed to Structural/Abstract syntax which captures only the essential structure.Concurrent programmingjust nowA programming paradigm where multiple computations execute in overlapping time periods, managing shared resources and coordination through synchronization primitives.Conditional expressionjust nowAn expression that selects between alternatives based on a boolean or Pattern matching (like if b then x else y or ternary b ? x : y).Congruencejust nowAn Equivalence relation that is preserved under a specific operation. That is, assume a congruence $\mathcal{C}$ and an operation $p$, we have $a\ \mathcal{C}\ b \iff p(a)\ \mathcal{C}\ p(b)$.Congruence rulejust nowA rule specifying how evaluation propagates into subterms, allowing reduction within a syntactic context while preserving the outer structure.Consequentjust nowThe part below the line in a typing rule - the Conclusion that follows when all Antecedents are satisfied (\"then\" part).Conservativejust nowA type checker that considers all possible executions rather than just actual ones - may reject programs that would run safely (false positives) because it can't know which branch will execute at runtConstantjust nowThe token itself is the value-the parser can extract it directly without consulting any environment or performing computationConstruct special formjust nowA built-in language primitive with special evaluation rules that cannot be implemented as a regular function (e.g., `if`, `lambda`, `define` in Lisp). In other words, special forms are necessary for cases where Derived forms do not suffice.Constructorjust now(Programming paradigm, Language feature/design) In languages with closures or prototypes, a function that returns objects of similar shapes.Constructor expressionjust now[Rocq] An expression that applies a constructor to arguments to build a value of an inductive type (like `S (S O)` for 2, or `Some 42` for an optional integer).Constructor expression constructorjust now[Rocq] An expression that applies a constructor to arguments to build a value of an inductive type (like `S (S O)` for 2, or `Some 42` for an optional integer).Constructor tagjust nowA runtime marker that distinguishes which variant of a Sum type a value belongs to, enabling Pattern matching to dispatch on the correct case. Not to be confused with Type variants, which are static properties.Contextjust nowNo description yetContext freejust nowA grammar where production rules depend only on a single non-terminal, not its surroundings - parsers handle this level; e.g., balanced parentheses, syntax structure.Context sensitivejust nowA grammar where production rules can depend on surrounding symbols (context) - type systems handle this level; e.g., \"variable must be declared before use\" requires checking context of the usage site.Contractjust nowProblem: When typed code is called from untyped code, the type checker can't guarantee arguments will have correct types - untyped code has no static checking.Coqjust nowTools: Rocq (formerly Coq)Core calculus languagejust nowA minimal formal language capturing the essential features of a paradigm or language, used to study semantics and prove properties without the complexity of full-scale syntax.Countable setjust nowA set that is either finite, or is infinite and there exists a bijection from itself into $\mathbb{N}$.Curry howard correspondencejust nowNo description yetCurry y combinatorjust now$$Curry y combinator z combinatorjust now$$Curryingjust nowThe act of turning a multi-parameter function into a Higher-order function that accepts one argument and returns a partially-applied version of the original function.Currying rocqjust nowNo description yetCursorjust nowNo description yetD39
Dimensional inference rule formatjust nowA style of formal definition that defines a set inductively as the smallest set closed under the rules - an element is in the set iff it can be derived by a finite Derivation tree of rule applications.Decidabilityjust nowA property of a problem or language where an algorithm exists that can always determine the correct yes/no answer in finite time for any input.Decidable propositionjust nowA proposition $P$ for which an algorithm exists that, in finite time, either produces a proof of $P$ or a proof of $\neg P$ - i.e., you can compute which side of $P \vee \neg P$ holds.Decision procedurejust nowAn algorithm that always terminates and correctly answers yes/no for any instance of a given problem class (like propositional satisfiability or type equivalence).Decreasing analysisjust now[Rocq] A termination check in Rocq that verifies recursive functions always call themselves on structurally smaller arguments, ensuring all computations terminate (required for logical consistency).Denotational semanticsjust nowA style of semantics that gives meanings to terms compositionally by mapping them to mathematical objects that possess interesting behaviors.Dependent typejust nowConsider the $\\text{head}$ function which returns the first item of a list.Derivabilityjust nowNo description yetDerivability judgmentjust nowNo description yetDerivablejust nowA property of an Evaluation statement/judgement that it can be derived using the evaluation rules in the calculus.Derivable evaluation statement judgementjust nowAn Evaluation statement/judgement is derivable if there is a Derivation tree conforming to the evaluation relation whose root is that evaluation statement.Derivationjust nowA finite composition of rules, starting with Axioms and ending with a desired Judgment.Derivation derivation treejust nowA specific visualization of a specific proof that $t \to t'$.Derivation forward chaining backward chaining bottom upjust nowNo description yetDerivation treejust nowA specific visualization of a specific proof that $t \to t'$.Derived formjust nowA construct that adds no expressive power but can be translated into more primitive forms, e.g., $\text{let}\ x = s\ \text{in}\ t$ desugars to $(\lambda x.\ t)\ s$.Derived queryjust nowNo description yetDesired property determinacy of one step evaluationjust nowA desirable property of a Lambda calculus where each term always evaluates to the same term in a single step.Desired property determinacy of one step evaluation relationjust nowA desirable property of a Lambda calculus where each term always evaluates to the same term in a single step.Desired property normal form implies valuesjust nowA desirable property of a Lambda calculus where there's no Stuck term. This property may not hold in most systems.Desired property termination of evaluationjust nowA desirable property of a Lambda calculus where every term all evaluates to a Normal form, whether they become Stuck term or Value. This property may not hold in most systems.Desired property termination of evaluation desired propertyjust nowA desirable property of a Lambda calculus where every term all evaluates to a Normal form, whether they become Stuck term or Value. This property may not hold in most systems.Desired property uniqueness of normal formsjust nowA desirable property of a Lambda calculus where every term always evaluates to the same Normal form. This property should hold in all deterministic systems.Desired property value is in normal formjust nowA desirable property of a Lambda calculus where every value is in Normal form. This property must hold in all system.Desugarjust nowThe process of transforming Syntactic sugar or high-level constructs into more primitive forms in the Core calculus/language, simplifying the interpreter or compiler implementation.Desugarerjust nowA Compiler phase or program that transforms Syntactic sugar into core language constructs, typically running before interpretation or further compilation stages.Dimensional analysisjust nowA static verification technique that encodes domain-specific properties (e.g., physical units, array bounds, indices) into types, ensuring operations respect these invariants by detecting mismatches at compile time rather than runtime.Directed acyclic graph dagjust nowNo description yetDivergent big omega combinatorjust nowFormula: $\Omega = (\lambda x.\ x\ x)\ (\lambda x.\ x\ x)$Divergent big omega combinator curry y combinatorjust nowFormula: $\Omega = (\lambda x.\ x\ x)\ (\lambda x.\ x\ x)$Divergent termjust nowA term that does not evaluate to a Normal form.Domainjust now(Set theory & Relation, Order & Lattice theory) A mathematical structure (typically a complete Partial order with a bottom element) used in Denotational semantics to model computation - enables reasoning about recursion, non-termination, and fixed points; values form a lattice where $\bot$ represents divergence/undefined.Domain theoryjust nowA branch of mathematics studying structured sets (domains) with partial orders and continuity, providing foundations for Denotational semantics - particularly for modeling recursion via Fixed-point combinators.Double negation eliminationjust nowholds. It asserts that if it is false that $A$ is false, then $A$ is true.Duck typingjust nowAn informal term for Structural typing - if an object has the required methods/properties (\"quacks like a duck\"), it can be used regardless of its declared type or class hierarchy.Dynamic dispatchjust nowA runtime mechanism that selects which method implementation to invoke based on the actual dynamic properties of the object, rather than the declared static properties of the reference, enabling polymorphic behavior. Contrast with Static dispatch.Dynamic scopejust nowThis is considered unambiguously wrong in language design - it makes programs unpredictable and tools unreliable.Dynamic semanticsjust nowThe meaning of programs in terms of their runtime behavior - how expressions evaluate, statements execute, and state changes over time.Dynamically sized type dstjust nowNo description yetE26
Elimination rulejust nowExample:Empty setjust nowA set with no element.Entailmentjust nowNo description yetEnumerated typejust nowA data type that defines a fixed set of named values (like enum Color { Red, Green, Blue }), enabling type-safe representation of discrete choices.Environmentjust now(Lambda calculus, Semantics) A finite map from variables to values, used to track substitutions during evaluation.Environment extensionjust nowThe operation $\\Gamma[x \\leftarrow t]$ that creates a new environment with all bindings from $\\Gamma$ plus variable $x$ bound to term/type/etc. $t$.Equivalencejust nowA Reflexive, Transitive and Symmetric relation.Error recoveryjust nowNo description yetEta equivalencejust nowA relation that relates a term to its Eta-expansion - $\lambda x.\ f\ x = \eta f$ when $x \notin FV(f)$ - capturing the principle that functions with identical input-output behavior are equivalent.Eta expansionjust nowThe transformation of a term $t$ to $\lambda x.\ t\ x$ where $x \notin FV(f)$ - the inverse of Eta-reduction, often used to delay evaluation or make function abstraction explicit.Eta reductionjust nowThe transformation of $\lambda x.\ t\ x$ to $t$ where $x \notin FV(f)$ - eliminating a redundant Lambda abstraction when a function simply passes its argument unchanged to another function.Evaluation reduction relationjust nowAn n-place relation on the set of terms in a calculus that represents computation, either Small-step/Structural operational semantics (SOS), Big-step/Natural operational semantics or something else.Evaluation reduction relation derivablejust nowAn n-place relation on the set of terms in a calculus that represents computation, either Small-step/Structural operational semantics (SOS), Big-step/Natural operational semantics or something else.Evaluation statement judgementjust nowA formal assertion of the form $t \to t'$ or $t \Downarrow v$, stating that a term reduces to another term or evaluates to a value under specific Inference rules.Evaluation strategyjust nowA specification of which Beta-redex/Reducible expression to reduce and in what order, determining how terms are evaluated (e.g., Call by value, Call by name, Normal order).Evaluation strategy strict eager evaluation strategy lazyjust nowA specification of which Beta-redex/Reducible expression to reduce and in what order, determining how terms are evaluated (e.g., Call by value, Call by name, Normal order).Evaluatorjust nowA program that turns programs into answersEvaluator interpreterjust nowNo description yetEventjust nowNo description yetEvent based parsingjust nowNo description yetEvidencejust nowNo description yetExpansionjust nowNo description yetExpressionjust now(Semantics, Syntax & Grammar, Language feature/design) A syntactic construct that evaluates to a value, as opposed to a Statement.Expression problemjust nowNeither paradigm naturally supports both dimensions of extensibility without modifying existing code or sacrificing Type safety. Solutions exist (type classes, object algebras, tagless final) but invoExpressivenessjust now(Language feature/design) The ease and directness of expressing programmer intent - a more expressive feature allows saying something concisely and naturally (e.g., pattern matching expresses variant dispatch more directly than chains of predicates + accessors; list comprehensions express transformations more naturally than explicit loops); distinct from computational power since both may be Turing-complete but differ in convenience.Extensible open recursionjust nowWhen utilizing the Class pattern to define classes with method calls referencing other methods, a recursion pattern that allows method references to be resolved at call site.F30
Falsyjust nowA value that evaluates as false in a boolean context despite not being literally false (like 0, null, \"\", or undefined in dynamic languages).Fieldjust nowA named data member of a class or object that stores part of the object's state, accessed via dot notation or accessor methods.Finite typejust nowA type with a bounded number of inhabitants (like bool with 2 or enum with fixed variants), often enabling exhaustive enumeration or decidable equality.First classjust nowNo description yetFirst class functional programming purejust nowThe status of an entity being a first-class citizen in a language - typically:First order variablejust nowA variable that ranges over data values (e.g., integers, booleans, records) - as opposed to Higher-order function variables which can hold functions or other computational entities.Fixed point combinatorjust nowTools: Rocq (formerly Coq)Fixityjust nowA syntactic property specifying an operator's position relative to its arguments: prefix (-x), infix (x + y), or postfix (x!).Flow analysisjust nowA static analysis technique that tracks how information propagates through a program's control flow - determining what facts hold at each program point based on paths taken.Flow sensitive typingjust nowSynonym for Flow typing - the type checker is \"sensitive\" to control flow, tracking how conditionals, assignments, and predicates refine types at different program points.Flow typingjust nowA type system feature where a variable's type changes based on control flow - after if (x != null), the type of x narrows from T | null to T.Formal derivability judgmentjust nowNo description yetFormal generic judgmentjust nowNo description yetFormal parameterjust nowThe variable declared in a function definition that receive values when called - placeholders in the function signature.Formal systemjust nowA mathematical framework consisting of a syntax for forming statements, axioms taken as given, and inference rules for deriving new statements from existing ones.Forward chainingjust nowA proof technique for Judgment forms that starts with an Axiom and tries to derive the desired judgment.Forward chaining backward chainingjust nowA proof technique for Judgment forms that starts with an Axiom and tries to derive the desired judgment.Forward chaining forward chaining searchjust nowA proof technique for Judgment forms that starts with an Axiom and tries to derive the desired judgment.Forward chaining searchjust nowA search strategy for a Derivation of a Judgment form that keeps track of the currently derivable judgments (initially the Axioms) and tries to expand the set using the rules at each step.Forward chaining search backward chaining searchjust nowA search strategy for a Derivation of a Judgment form that keeps track of the currently derivable judgments (initially the Axioms) and tries to expand the set using the rules at each step.Free variablejust nowA variable that is not bound by any enclosing $\lambda$. Contrast with Bound variable.Fresh renamingjust nowGiven a set of variables $\\mathcal{X}$ and a finite sequence of variables $\\vec{x}$, a bijection $\\rho : \\vec{x} \\leftrightarrow \\vec{x}'$ between $\\vec{x}$ and $\\vec{x}'$, where $\\vec{x}'$ is fresh fFresh variablejust nowGiven a set of variable $\mathcal{X}$, a Variable $v \notin \mathcal{X}$.Fresh variable abstract syntax tree astjust nowGiven a set of variable $\mathcal{X}$, a Variable $v \not\in \mathcal{X}$.Full beta reductionjust nowIn Pure/Untyped lambda calculus, this strategy is defined by the following rules:Functionjust now(Language feature/design) A reusable piece of code that returns a result.Function definitionjust nowA syntactic construct that declares a function by specifying its name (optionally), Formal parameters, and body - establishing a binding between the name and the corresponding abstraction.Function headerjust nowThe declarative part of a function that specifies its name, Formal parameters, and return type (if any), without the body implementation.Function rocqjust nowUse the `Fixpoint` definition. For example:Functional programmingjust nowA programming paradigm centered on pure functions, immutability, and expressions rather than statements, treating computation as evaluation of mathematical functions.G16
Gallinajust nowA Functional programming language (Rocq's specification language) that allows writing purely functional programs and formal proofs, using Dependent type to express precise logical properties.Garbage collectionjust nowAn Automatic memory management technique that identifies and reclaims Heap-allocated memory no longer reachable by the program, freeing the programmer from explicit deallocation and preventing memory leaks and dangling references.General judgmentjust nowNo description yetGeneric derivabilityjust nowNo description yetGeneric derivability judgmentjust nowNo description yetGeneric derivationjust nowNo description yetGeneric general judgmentjust nowNo description yetGeneric inductive definitionjust nowNo description yetGeneric rulejust nowNo description yetGenericityjust nowNo description yetGlobal hypothesisjust nowNo description yetGlobal variablejust nowNo description yetGoaljust nowTools: Rocq (formerly Coq)Goal directedjust nowThe property of an algorithm that is aware of its goal and uses that knowledge to take educated steps towards the goal, or in the case of Backward chaining search, starting from the goal, and working backwards towards the Axioms.Gradual typingjust nowFully untyped <---------------> Fully typedGradual typing macro gradual typing micro gradual typingjust nowAn approach that allows mixing typed and untyped code in the same program, enabling incremental migration from dynamic to static typing.H15
Haltjust nowThe terminal state of an Abstract machine reached when the current term is in Normal form (i.e., no evaluation rule applies), signaling completion of evaluation.Heapjust nowA region of a process's memory used for dynamic allocation at runtime, growing as needed and managed explicitly (via malloc/free) or by a Garbage collection - as opposed to the stack which handles fixed-size, short-lived local variables and call frames.Heap addressjust nowAn address on the Heap.Higher order contractjust nowContracts on values that are themselves functions (or contain functions), presenting unique challenges because the contract cannot be fully checked immediately.Higher order functionjust nowA function that accepts or returns another function.Hindley milner systemjust nowA type system with complete type inference via constraint generation and unification - automatically determines the most general (principal) type for all expressions without annotations; basis for ML,Hoare logicjust nowA formal system for reasoning about program correctness using triples {P} C {Q} (precondition, command, postcondition) to specify and verify imperative programs.Hoare type theoryjust nowA type theory that integrates Hoare-style specifications into types, allowing pre/postconditions and invariants to be expressed and checked within a dependently typed language.Host languagejust nowThe language a compiler is implemented in.Hygienic macrojust nowHygienic macros are analogous to Lexical/Static scope for Macros: Macro variables are not just names, but rather binding information records.Hypothesisjust now(Formal system, Proof/Reason technique, Language feature/design) [Rocq] A named assumption in the proof context that can be used to justify proof steps, introduced by tactics like `intros` or `assert`.Hypothetical inductive definitionjust nowNo description yetHypothetical judgmentjust nowNo description yetHypothetical rulejust nowNo description yetHypothetical rule inductionjust nowNo description yetI40
Identity combinatorjust nowFormula: $\text{id} = \lambda x.\ x$If splittingjust nowA type system mechanism where conditionals narrow union types based on predicates - after if (mt? t), the type of t refines from BT (union) to just mt in that branch, implementing Flow-sensitive typinImmediately invoked function expression iifejust nowExample: Parallel/Simultaneous let in Scheme is actually a Syntactic sugar for IIFE.Implicit formjust nowNo description yetImportjust now[Rocq] A command in Rocq:(/programming-language-theory/concepts/rocq) that brings names from a loaded module into the current namespace, allowing unqualified access (often combined as `Require Import`).Import requirejust nowNo description yetInadmissiblejust nowNo description yetIncomplete syntax treejust nowNo description yetIncremental computationjust nowNo description yetIndexed operatorjust nowA family of operators $o$ indexed by symbols $u$, so that $o[u]$ is an operator when $u$ is an available symbol.Induction on derivationsjust nowAn induction technique in which to prove a specific property about a Derivation, we take the Inductive hypothesis is that every smaller derivations satisfy that property.Inductive conclusionjust now$$Inductive definitionjust nowTools: Rocq (formerly Coq)Inductive definition 2 dimensional inference rule formatjust nowA definition technique that specifies a set or type by its base cases and rules for building new elements from existing ones.Inductive definition functionjust nowA definition technique that specifies a set or type by its base cases and rules for building new elements from existing ones.Inductive definition judgment formjust nowA definition technique that specifies a set or type by its base cases and rules for building new elements from existing ones.Inductive definition termjust nowA definition technique that specifies a set or type by its base cases and rules for building new elements from existing ones.Inductive hypothesisjust now$$Inductive typejust nowTools: Rocq (formerly Coq)Inference rulejust now(Logic) A formal statement consisting of Premises and a Conclusion, asserting that if all premises hold, the conclusion may be derived.Infinite typejust nowA type that has infinitely many inhabitants (like nat, string, or list), as opposed to finite types like bool or enums with fixed members.Infixjust nowA Fixity where an operator appears between its two arguments (like x + y), as opposed to prefix or postfix.Inheritancejust nowA mechanism where a class (subclass) derives properties and behaviors from another class (superclass), enabling code reuse and establishing an \"is-a\" relationship between types. This coupling betweenInheritance subtypingjust nowNo.Input queryjust nowNo description yetInstance of a rule schemejust nowSynonymous with Instance of an inference rule.Instance of an inference rulejust nowA specific substitution of the rule's Metavariables with concrete terms, yielding a particular Derivation step.Instance of the judgment formjust nowA Judgment form applied with one or more values. For a judgment form $-\ J$ and a value $a$, it is written as $a\ J$ or $J\ a$.Internerjust nowNo description yetInterning tablejust nowNo description yetInterpretationjust nowA semantic mapping that assigns meaning to a Representation (e.g., 0b101 can interpret as 5 in binary or a bit pattern).Interpretation functionjust nowA function mapping syntactic terms to mathematical objects (denotations) in a Semantic domain, assigning meaning compositionally based on the structure of terms.Interpreterjust nowMathematically, denote $\mathcal{P} L$ as the set of programs written in the language $L$ and $V$ the set of all possible values, an interpreter is a function $I: \mathcal{P} L \to V$.Intro patternjust now[Rocq] A tactic modifier in Rocq:(/programming-language-theory/concepts/rocq) that destructures hypothesises as they're introduced (like `intros [x y]` to unpack a pair or `intros [H|H]` for a disjunction).Introduction rulejust nowExample:Intuitionistic constructive logicjust now\\frac{A \\quad B}{A \\land B} & & (\\land\\text{-intro}) \\\\ \\\\Involutionjust nowA function that is its own inverse, satisfying f(f(x)) = x (like negation on booleans or reversing a list twice).Involutivejust nowA property of a function where applying it twice returns the original value (i.e., f(f(x)) = x).Iterated inductive definitionjust nowAn Inductive definition technique that specifies a set of elements as the strongest sets closed under a set of Inference rules - each inference rule may only refer to already defined sets or the currently defined one.Iterated inductive definition simultaneous inductivejust nowAn Inductive definition technique that specifies a set of elements as the strongest sets closed under a set of Inference rules - each inference rule may only refer to already defined sets or the currently defined one.J6
Joinjust nowIn the context of a Partial order, the least upper bound of a set $S$, denoted $\bigvee S$.Judgmentjust now(Logic) The mental act of affirming or denying a Proposition is true.Judgment assertion judgment form judgment form instance sjust nowTypically written as $- \ J$ (for unary relation).Judgment formjust nowSynonymous with an n-place relation. For a unary relation/predicate, a judgment form is usually written as $J\\ -$ or $-\\ J$, with $-$ being a placeholder for some value drawn from the domain of the prJudgment judgment formjust nowSynonymous with an n-place relation. For a unary relation/Predicate, a Judgment form is usually written as $J\ -$ or $-\ J$, with $-$ being a placeholder for some value drawn from the domain of the predicate.Just in time jit compilationjust nowAn Evaluator that starts out as an Interpreter but includes a monitor to detect, compile and utilize compiled hot code.L28
Labeled treejust nowSynonymous with Abstract syntax tree (AST).Lambda abstractionjust nowA Lambda term of the form $\lambda x.\ t$ - a function that binds variable $x$ over body $t$.Lambda abstraction lambda calculusjust nowA Lambda term of the form $λx.\ t$ - a function that binds variable $x$ over body $t$.Lambda calculusjust nowA minimal formal system for expressing computation using only variable binding and function application, yet serves as a foundation that can be extended with types, effects, recursion primitives, and other constructs to form the basis of modern programming languages.Lambda expressionjust nowA syntactic construct denoting an anonymous function, consisting of a list of Formal parameters and a body - e.g., $\lambda x.\ t$ or $(\text{lambda}\ (x)\ t)$.Lambda termjust nowAny expression in the Lambda calculus grammar: a variable, an Lambda abstraction, or an application.Language safetyjust now(Language feature/design, Runtime) According to Types and programming languages, from the view of portability, a language whose behavior can be entirely determined by its programmer's manual, that is, it is not subject to the internals of the specific machine it runs on.Language safety partialityjust nowAccording to Types and programming languages, a language that protects its own abstraction, that is, it is mostly impossible to corrupt the run-time’s data structure and program’s data structure (although there can be escape hatches to perform unsafe operations).Law of excluded middle lemjust nowholds. It asserts that every statement is either true or false, with no middle ground.Lazy evaluation strategyjust now(Language feature/design) An Evaluation strategy in which the argument is not evaluated before substituted into the function call.Left left lambdajust now((lambda (x) body) arg)Lexical analysisjust now(Syntax & Grammar, Linguistics) The process of classifying texts into Syntactic categorys.Lexical analysis parsingjust nowA step in the Compiler that involves converting texts into sequences of Tokens. This typically involves:Lexical static scopejust nowA Binding resolution strategy where a variable's binding is determined by its textual position in the source code - the enclosing Scope at the point of definition, not the call site at runtime.Lexicographic orderjust nowA total ordering on sequences that compares elements position-by-position from left to right, with the first differing position determining precedence - like dictionary ordering of words.Lexicographic order principle of lexicographic inductionjust nowA total ordering on sequences that compares elements position-by-position from left to right, with the first differing position determining precedence - like dictionary ordering of words.Lifetimejust nowNo description yetLight parsingjust nowNo description yetLinkjust nowWhat do you want to grasp from this question?Liskov substitution principle lspjust nowA design principle for OO inheritance stating that subtypes must preserve behavioral contracts of supertypes, ensuring code using parent class works correctly with any child class - preventing bugs frLiteraljust nowSynonymous with syntactic Constant.Local binding formjust now; Local binding - x only exists inside the letLocal formjust nowNo description yetLocal hypothesisjust nowNo description yetLocal variablejust nowA variable declared within a Block or function whose Scope and Lifetime are limited to that region - inaccessible from outside and typically deallocated when the block exits.Logicjust nowA Formal system for reasoning about truth, validity, and inference, defining syntax for propositions and rules for deriving conclusions.Logical derivationjust nowA step-by-step proof showing how a conclusion follows from premises using Inference rules - each step applies a rule to previous steps; in type systems, a Derivation tree is a derivation proving that anLogical systemjust nowA formal framework comprising a syntax (well-formed formulas), Axioms, and Inference rules that together determine which statements are Derivable.M32
Macrojust nowA syntactic pattern that is expanded into other code at compile time via Macro expansion, enabling metaprogramming by allowing code to generate or transform other code before execution.Macro definition hazard duplicationjust nowA Macro pitfall where an expression passed as argument is evaluated multiple times in the Macro expansion, causing unintended repeated Side-effects or performance issues.Macro expansionjust nowA compile-time code transformation where macro invocations are replaced by their expanded definitions, enabling Syntactic abstraction and code generation before regular compilation.Macro gradual typingjust nowA Gradual typing approach where typed and untyped code exist as two separate sibling languages that interact only at module boundaries, typically requiring Blame tracking.Macro hygienic macrojust nowA Macro system that automatically renames variables to prevent accidental Variable capture, ensuring that identifiers introduced by the macro don't clash with identifiers at the call site.Macro parenthetical languagejust nowNo description yetMacro side effectjust nowNo description yetMacro systemjust nowA language facility that provides programmable syntax transformations through Macros, enabling users to define new syntactic forms that expand into existing language constructs at compile time.Manglingjust nowNo description yetMap reducejust nowA Programming model that processes large datasets by applying a function to each element (map) then combining results with an associative operation (reduce), enabling parallelization.Match armjust nowNo description yetMathematical inductionjust nowFormally, assume $n\ \text{nat}$ means that $n$ is a natural number. To prove that whenever $n\ \text{nat}$, we have $\mathcal{P}(n)$, it's sufficient to show that:Meetjust nowIn the context of a Partial order, the greatest lower bound of a set $S$, denoted as $\bigwedge S$ .Message passingjust now(define msg (obj name . args)Meta mathematicsjust nowThe study of mathematical systems themselves using mathematical methods - analyzing properties like consistency, completeness, and decidability of formal theories.Metalanguagejust nowThe language used to describe, define, or reason about another language (Object language) - e.g., English and mathematical notation when specifying Lambda calculus.Metatheoryjust nowThe study of properties about a Formal system (e.g., Soundness, Completeness, termination), using external reasoning to prove facts about the system itself.Metavariablejust nowA variable in the Metalanguage that ranges over elements of a Syntactic category in the object language - e.g., $t$ ranging over terms, $v$ over values, $x$ over variables.Methodjust nowA function defined within a class that operates on instances of that class, typically bound to and having implicit access to the object's state through this or self.Method functionjust nowA Method is a function that gets bound to an Object.Micro gradual typingjust nowA Gradual typing approach where type annotations can be added to any subset of variables within the same code, freely mixing typed and untyped expressions.Mixfixjust nowA notation to write down an instance of an N-place relation. For example, for a ternary relation $R$, one can write $\Gamma \vdash t : T$ to denote $(\Gamma, t, T) \in R$.Mixinjust nowA function that transforms a class into another class, typically adding behaviors to it assuming the class conforms to an interface, similar to a Class extension.Model checkerjust nowAn automated verification technique that exhaustively explores the state space of a (typically finite-state) system to detect violations of specified properties such as safety, liveness, or protocol correctness.Model checker type system runtime monitoringjust nowAn automated verification technique that exhaustively explores the state space of a (typically finite-state) system to detect violations of specified properties such as safety, liveness, or protocol correctness.Modularizationjust nowPapers: On the Criteria To Be Used in Decomposing Systems into Modules (../../Papers/Papers/On%20the%20Criteria%20To%20Be%20Used%20in%20Decomposing%20Systems%20%2031baa8fcd08880429536c92add4ffb42.md)Modulejust nowPapers: On the Criteria To Be Used in Decomposing Systems into Modules (../../Papers/Papers/On%20the%20Criteria%20To%20Be%20Used%20in%20Decomposing%20Systems%20%2031baa8fcd08880429536c92add4ffb42.md)Module systemjust nowA language feature that organizes code into namespaced units with controlled visibility, enabling encapsulation, separate compilation, and abstraction through signatures/interfaces.Multi step evaluation relationjust nowThe Reflexive closure and Transitive closure of the One-step evaluation relation. The relation is often denoted as $\to^$.Multiple inheritancejust nowAn Inheritance model where a class can inherit from multiple parent classes, combining their behaviors but potentially introducing ambiguity (The diamond problem) when parents share method names.Mutablejust nowThe property of an entity (variable, data structure, reference) whose contents can be modified in place after creation.Mutationjust nowThe act of modifying a value in place at a memory location, rather than producing a new value - introducing State changes that depend on evaluation order and complicating equational reasoning.N12
N place relationjust nowGiven $n$ sets $X 1, X 2, ..., X n$, the subset of the Cartesian product $X 1 \times X 2 \times ... \times X n$.Name combination algebrajust nowThe set of rules governing how names interact when combining program fragments, addressing whether bindings Shadowing, conflict, or merge (central to understanding Substitution, Scope, and module composition).Natural deduction stylejust nowA presentation of Logical systems where Inference rules are organized into Introduction rule and Elimination rule for each connective, with proofs structured as trees that introduce and discharge assumptions.Newtype idiomjust nowNo description yetNodejust nowNo description yetNominal typejust nowA type identified by its name - two types are equal only if they have the same declared name, regardless of structure.Nominal typingjust nowA type system where Type compatibility is determined by explicit declarations (class names, inheritance hierarchy), not structure - class A and class B are different even if identical in shape.Nominal typing structural typingjust nowA type system where Type compatibility is determined by explicit declarations (class names, inheritance hierarchy), not structure - `class A` and `class B` are different even if identical in shape.Nonsensical termjust nowExample: In the Untyped calculus of booleans and numbers, the followings are nonsensical:Normal formjust nowA term that cannot be evaluated further.Normal form valuejust nowA term that cannot be evaluated further.Normal orderjust nowIn pure lambda calculus, this strategy is defined by the following rules:O16
Objectjust nowA multi-entrypoint Closure that can be accessed using Message passing.Object closurejust nowAn Object is a Closure with multiple entrypoints.Object lambda expressionjust nowNo description yetObject languagejust nowThe formal language being defined, analyzed, or reasoned about - as opposed to the Metalanguage used to describe it.Object memberjust nowA component of an object, either a Field (data) or a Method (behavior).Object patternjust now(define oOccurrence typingjust nowA type system technique where a variable's type can differ at each occurrence (use) based on what predicates have been checked - the same variable x can have type Number in one branch and String in another. Synonymous with Flow typing.On demand computationjust nowNo description yetOne step evaluation relationjust nowA relation defining a single atomic reduction, mapping a term to its immediate successor by applying exactly one reduction rule. The relation is denoted using the symbol $\to$.One step evaluation relation partial functionjust nowA relation defining a single atomic reduction, mapping a term to its immediate successor by applying exactly one reduction rule. The relation is denoted using the symbol $\to$.Operational semanticsjust nowA style of semantics that defines the meaning of programs by syntactically transforming terms according to reduction rules, specifying execution either step-by-step (Small-step/Structural operational semantics (SOS)) or as a direct relation to final values (Big-step/Natural operational semantics).Operational semantics untyped calculus of booleans andjust nowA style of semantics that defines the meaning of programs by syntactically transforming terms according to reduction rules, specifying execution either step-by-step (Small-step/Structural operational semantics (SOS)) or as a direct relation to final values (Big-step/Natural operational semantics).Operatorjust nowAccording to Practical foundations for programming languages , an interior node of an Abstract syntax tree (AST), with a specified Arity $(s 1;\dots; s n)s$, for $s i \in \mathcal{S}$ - the set of Sorts.Operator abstract syntax tree astjust nowNo description yetOperator arityjust nowNo description yetOrdered variadic treejust nowNo description yetP49
Pair encodingjust nowEncoding:Parallel simultaneous letjust now(let ([x 1]Parametric general judgmentjust nowNo description yetParenthetical languagejust now(define-syntax-rule (or a b) (if a a b))Parsingjust now(Compiler implementation) The process of converting Concrete/Surface syntax into Abstract syntax tree (AST)s.Partial functionjust nowA Binary relation $R$ such that if $s\ R\ t 1$ and $s\ R\ t 2$ then $t 1 = t 2$.Partial orderjust nowA Binary relation that is Transitive, Reflexive and Antisymmetric.Partialityjust nowThe property of a computation that may not terminate or produce a result for all inputs. Partial functions are undefined for some inputs, unlike Total functions which always return a value.Patternjust nowA structural template that matches values by shape (using constructors, variables, or wildcards), enabling destructuring and case analysis in match expressions.Pattern matchingjust nowA language construct that deconstructs Algebraic data type values by variant, binding fields to variables and enabling the type checker to refine types in each branch - safer than raw predicates + accessors.Polymorphic type systemjust nowA type system that allows types to contain variables (like List<T>, $\forall$ a. a $\to$ a), enabling one definition to work across many types through type abstraction.Powersetjust nowDefinition: $\mathcal{P}(S) = \{ s\ |\ s \subseteq S \}$ .Pratt parsingjust nowNo description yetPrecedencejust nowA parsing rule that determines which operator binds tighter (e.g., `` before `+` makes `1 + 2 3` parse as `1 + (2 3)`).Predicatejust nowAn unary n-place relation $P$, $(s) \in P$ is typically written as $P(s)$.Predicate typejust nowA function type annotated with what it proves when returning true - e.g., (-> Any Boolean : mt) means \"takes anything, returns Boolean, and when true, input was mt.\" Essentially, a type of a Type predPremisejust nowAn antecedent judgment in an Inference rule that must be Derivable for the rule to derive its Conclusion.Preorderjust nowA Binary relation that is Reflexive and Transitive.Primordial blockjust nowThe implicit outermost scope containing built-in definitions (e.g., primitive types, standard functions) that encloses the global scope, making built-ins available without explicit import.Principle of complete inductionjust nowA proof technique where the inductive step assumes the property holds for all predecessors (not just the immediate one), deriving the property for the current element.Principle of lexicographic inductionjust nowA proof technique using Lexicographic order on tuples of measures, allowing induction where each recursive step decreases the tuple lexicographically - any component may increase if an earlier component strictly decreases.Principle of ordinary inductionjust nowA proof technique with a base case and an inductive step that assumes the property holds for the immediate predecessor to prove it for the successor.Private memberjust nowA class member that is only accessible from within the class itself, providing encapsulation by hiding implementation details from external code.Procedural functional abstractionjust nowThe principle of encapsulating a computation behind a named interface, hiding implementation details and allowing reuse by parameterizing over inputs.Procedurejust nowA subroutine that performs actions primarily for Side-effects rather than returning a value. Unlike functions, procedures emphasize imperative steps over computation of results.Programjust nowThe start symbol representing a complete, well-formed unit of code - the top-level nonterminal from which all valid programs are derived.Programming modeljust nowA conceptual framework defining how computations are structured and executed (like shared memory, Message passing, or Map-Reduce), abstracting over hardware details.Programming paradigmjust nowA style or philosophy of programming characterized by its core concepts and patterns (like functional, imperative, object-oriented, or logic programming).Proliferationjust nowNo description yetProofjust nowTools: Rocq (formerly Coq)Proof assistant proverjust nowTools: Rocq (formerly Coq)Proof by case analysisjust nowTools: Rocq (formerly Coq)Proof by rewritingjust nowNo description yetProof by simplificationjust nowTools: Rocq (formerly Coq)Proof checkerjust nowA program that verifies whether a given proof is valid according to the rules of a Formal system, confirming that each step correctly follows from the Axioms and Inference rules.Proof techniquejust now(Formal system, Proof/Reason technique, Language feature/design, Programming paradigm) [Rocq] In Rocq, a conceptual strategy for proving goals (like induction or case analysis), typically realized by corresponding tactics.Proper rulejust nowAn Inference rule that is not an Axiom, in other words, has at least one Premises.Propositionjust nowIn the context of Intuitionistic/Constructive logic.Prototypejust nowAn object that serves as a template for creating other objects through cloning, used in prototype-based languages like JavaScript as an alternative to class-based Inheritance, generalizing class-based inheritance.Prototype classjust nowCreate a prototype object that contains all the shared methods and default properties.Purejust nowThe property of a function or computation that has no side effects and always returns the same output for the same input, making it referentially transparent.Pure type systemjust nowA general framework parameterizing typed lambda calculi by a triple (sorts, axioms, rules), unifying systems like Simply typed lambda calculus, System F, and the Calculus of inductive construction under a single formalism.Pure untyped lambda calculusjust now$$Pure untyped lambda calculus call by valuejust now$$Pure untyped lambda calculus church numeraljust now$$Pure untyped lambda calculus curryingjust now$$Pure untyped lambda calculus pair encodingjust now$$Pure untyped lambda calculus runtime error stuck termjust now$$Pure untyped lambda calculus syntactic categoryjust now$$R42
Rangejust nowSynonymous with Codomain.Read eval print loop repljust nowA program that provides an interactive interface for programmers to interact with a programming language in an adhoc and highly-responsive fashion. The name represents the typical phases of this interaction: The program reads the input from the user, evaluates it, prints out the result and loops.Read eval print loop repl compiler interpreterjust nowA program that provides an interactive interface for programmers to interact with a programming language in an adhoc and highly-responsive fashion. The name represents the typical phases of this interaction: The program reads the input from the user, evaluates it, prints out the result and loops.Recursive descentjust nowNo description yetRecursive descent parserjust nowNo description yetRecursive letjust now(letrec ([fact (lambda (n)Recursive macrojust nowA Macro that can expand to code containing further macro invocations, including calls to itself. Enables powerful metaprogramming but requires careful handling to ensure termination.Recursive typejust nowA type whose definition reference itself.Refined typejust nowA type that carries additional constraints beyond the base type, such as \"positive integers\" or \"non-null strings\". Enables more precise specifications and stronger compile-time guarantees.Reflexivejust nowA property of a Binary relation $R$ on a set $T$ such that $t\ R\ t$ for every $t \in T$.Reflexive closurejust nowThe smallest superset of a set that is reflexive.Reflexive transitivejust nowNo description yetReflexivityjust nowTools: Rocq (formerly Coq)Renamingjust nowNo description yetRepresentationjust nowA concrete encoding of abstract data (e.g., the numeral 5 can be represented as \"101\", S(S(S(S(S O)))), or 0x05).Requirejust now[Rocq] A command in Rocq that loads a compiled module into memory, making its contents available but not directly accessible without qualification.Retrofitted type systemjust nowA Type system added to an existing untyped language after the fact - must accommodate existing idioms and codebases rather than designing types from scratch.Rice s theoremjust nowA theorem stating that any non-trivial semantic property of programs is Decidability - we cannot automatically determine arbitrary properties about what programs compute (e.g., "does this function always return a positive number?"), which is why type systems must be conservative approximations.Rocqjust nowTools: Rocq (formerly Coq)Rocq axiomjust nowNo description yetRocq church numeraljust nowNo description yetRocq constructor function computation rulejust nowA Constructor expression is an expression constructed using a Constructor, effectively creating a member of a set represented by a type.Rocq dependent typejust nowNo description yetRocq gallinajust nowNo description yetRocq inductive definitionjust nowIt allows defining Algebraic data types in Rocq, including Recursive types.Rocq kerneljust nowTools: Rocq (formerly Coq)Rocq tacticjust nowNo description yetRocq truthyjust nowThe first constructor of an inductive type that has two constructors.Roslynjust nowNo description yetRulejust nowShort-hand for Inference rule.Rule inductionjust now$$Rule schemajust nowAn parameterized inference rules with Metavariables that can be instantiated to Concrete rules or Inference rules.Rule schema inference rule concrete rule instance of anjust nowAn parameterized inference rules with Metavariables that can be instantiated to Concrete rules or Inference rules.Rule schemejust nowSynonymous with Rule schema.Rule scheme inference rule metavariablejust nowSynonymous with Rule schema.Runtime errorjust now(Runtime) An error that happens at runtime.Runtime monitoringjust nowA dynamic verification technique that inserts observers to track program execution and detect when behavior deviates from specified properties (e.g., Contracts, protocols, temporal constraints).Runtime type dispatchjust nowA pattern typically associated with Union types in which the type of a value is checked so that specialized logic can be carried out. Flow-sensitive typing is especially useful.Runtime type errorjust nowAccording to Types and programming languages, the class of undefined or undesirable behaviors that a Type system is designed to prevent - whether they are actually eliminated depends on the soundness of the type system.Runtime type information rttijust nowA mechanism that allows the reflection of the type of a value at runtime.Rust cratejust nowNo description yetRust modulejust nowNo description yetS75
S expression symbolic expressionjust nowA notation for nested list-structured data, defined recursively as either an atom (e.g., number, symbol) or a parenthesized list of S-expressions - the uniform syntax used in Lisp for both code and data.Safe sound type systemjust nowA Type system where the static judgment "term $t$ has type $T$" implies a corresponding semantic property at runtime - formalized as: if the type system accepts a program, execution cannot produce behaviors the types claim to exclude.Safety checkjust nowA mechanism, either carried out by the runtime to enforce Language safety / avoid Runtime type error or by programmers to avoid Runtime error.Sat solverjust nowA Decision procedure that determines whether a propositional boolean formula has a satisfying assignment, foundational to many automated reasoning tools.Scopejust now(Semantics) The region of the code that a Binding takes effect.Scope bindingjust nowNo description yetSelf referencejust now(Programming paradigm) A technique in the Class pattern that allows members of a class to reference their owner objects.Self replicatorjust nowExample:Semantic domainjust nowThe mathematical structure (e.g., sets, functions, lattices) in which terms are given meaning by a Denotational semantics.Sentence diagramjust nowA syntactic structure of a given sentence.Sequencejust nowAn ordered collection of elements indexed by natural numbers - formally, a function from $\mathbb{N}$ to some set, denoted $(a 0, a 1, a 2, ...)$ or $(a i) i\in\mathbb{N}$.Sequential evaluationjust nowAn execution model where expressions or statements are evaluated one after another in a specified order, with each completing before the next begins - the default in imperative languages, contrasted with parallel or concurrent evaluation.Set comprehensionjust nowExample: $\mathbb{Q} = \{\displaystyle \frac{p}{q}\ |\ p \in \mathbb{Z} \land q \in \mathbb{Z} \land q \neq 0 \}$.Set differencejust nowDefinition: $R - Q = \{x \ | \ x \in R \land \ x \notin Q \}$.Shadowingjust nowThe phenomenon when an inner Binding uses the same name as an outer binding, making the outer one inaccessible within the inner Scope.Side effectjust nowAn observable interaction with the outside world or modification of state beyond returning a value, such as I/O, mutation, or exceptions.Simply typed lambda calculusjust nowThe foundational typed lambda calculus where each Lambda abstraction explicitly annotates its parameter with a type, providing a basis for more advanced type systems while guaranteeing termination.Simultaneous inductive definitionjust nowA definition technique that define more than one sets at once as a collection of Inference rules to determine membership of the elements of the sets - each inference rule shall refer to the sets in its Premises and its Conclusions.Small omega combinatorjust nowA Combinator defined as $\omega = \lambda x.\ x\ x$, useful in many patterns, such as Extensible/Open recursion.Small step structural operational semantics sosjust nowA style of semantics which defines evaluation via Evaluation statement/judgement of the form $t \to t'$, specifying how a term reduces by one atomic step at a time until reaching a Normal form.Smt solverjust nowA Decision procedure that determines satisfiability of formulas in first-order logic with theories (like arithmetic, arrays, bit-vectors), extending SAT solver to richer domains.Sortjust nowA Syntactic category that classifies Abstract syntax tree (AST)s. Roughly a type for ASTs.Soundjust nowThe adjective form of Soundness.Soundnessjust nowNo description yetStablejust nowNo description yetStatejust nowThe complete configuration of an Abstract machine at a point during evaluation, comprising the current term and any auxiliary data (e.g., Environment, store, stack). In Pure/Untyped lambda calculus, the state is simply a Lambda term.Statementjust nowA Term that does not evaluate to a value, but rather cause a Side-effect.Static analysisjust nowProgram analysis performed without executing the code, including type checking, dataflow analysis, and abstract interpretation. Can detect certain errors and properties before runtime.Static disciplinejust nowAn approach where Static analysis and other analyses are performed before program execution, catching errors at compile time rather than runtime. Contrasts with dynamic discipline.Static dispatchjust nowMethod resolution that occurs at compile time based on some known (may be imprecise) static properties (such as types) of the receiver, as opposed to Dynamic dispatch which resolves at runtime based on the actual dynamic properties.Static memberjust nowA field or method that belongs to the Class itself rather than to instances, shared across all objects of that class and accessible without creating an instance.Static semanticsjust nowThe meaning of programs determinable without execution - type checking, scope resolution, and other compile-time analyses that reject ill-formed programs.Static typejust nowA type that is determined and checked at compile time, before the program runs, as opposed to dynamic types which are checked at runtime.Strength reductionjust nowNo description yetStrict eager evaluation strategyjust now(Language feature/design) An Evaluation strategy such that an argument is evaluated before passing into the function call.String internerjust nowNo description yetStrong normalizationjust nowThe property of a language written in which every program always terminates.Structuraljust nowNo description yetStructural abstract syntaxjust now(Syntax & Grammar) According to Practical foundations for programming languages, the program's tree structure (Abstract syntax tree (AST)) showing how phrases are built from Operators and subphrases.Structural abstract syntax concrete surface syntaxjust now(Syntax & Grammar) According to Practical foundations for programming languages, the program's tree structure (Abstract syntax tree (AST)) showing how phrases are built from Operators and subphrases.Structural inductionjust nowA proof technique for inductively defined structures, where a property is shown for all elements by proving base cases and proving composite cases assuming the property holds for all immediate sub-structures.Structural induction modulo fresh renamingjust nowTo show that $\\mathcal{P}\\mathcal{X}$ holds for every $a \\in \\mathcal{B}[\\mathcal{X}]$, it is enough to show the following:Structural propertyjust nowNo description yetStructural recursionjust nowA recursion scheme that decomposes data along its Constructors, guaranteeing termination by recursing only on structurally smaller subterms.Structural rulejust nowNo description yetStructural typejust nowA type defined by its shape (fields, methods, signatures) rather than its name - two types are equal if they have the same structure.Structural typingjust nowA type system where Type compatibility is determined by structure, not name - any value with matching shape satisfies the type, regardless of declared class or origin.Structuralityjust nowNo description yetStuck termjust nowA Lambda calculus term that is in Normal form but not a value.Stuck term value normal formjust nowA Lambda calculus term that is in Normal form but not a value.Subclassjust now(Semantics, Language feature/design, Programming paradigm) A Class that extends a parent class.Subgoaljust nowTools: Rocq (formerly Coq)Substitutabilityjust nowThe semantic/behavioral property that one value can safely replace another without breaking program correctness, of which Type compatibility is a static approximation of.Substitutionjust nowNo description yetSubstitution subjectjust nowA variable to which an object is substituted in.Substitution subject substitution targetjust nowA variable to which an object is substituted in.Substitution targetjust nowThe parameterized expression whose variables are substituted with objects.Subtypejust nowA type $X$ that can be used wherever type $Y$ is expected - $X$ is \"more specific\" than $Y$.Subtypingjust nowThe Type system mechanism that defines and enforces when substitution is allowed between types.Subtyping relationjust nowWritten $X <: Y$, a formal ordering on types meaning "$X$ is a Subtype of $Y$" - $X$ substitutes for $Y$.Sum of products sopjust nowThe structure of Algebraic data types - sum because variants combine via "or" (one of mt or node), product because each variant's fields combine via "and" (a node has v and l and r).Sum typejust nowAn algebraic datatype with multiple Type variants combined via "or" - a value is one of the variants, each with its own Constructor tag (e.g., BT = mt | node).Sum type union typejust nowAn algebraic datatype with multiple Type variants combined via "or" - a value is one of the variants, each with its own Constructor tag (e.g., `BT = mt | node`).Supertypejust nowIf $X$ is a Subtype of $Y$ then $Y$ is a supertype of $X$.Surface languagejust nowThe user-facing syntax of a programming language, including Syntactic sugar and conveniences, as opposed to the Core calculus/language that programs are desugared into.Symboljust nowAs per Practical foundations for programming languages's terminology, an index to the families of operators. Given an Indexed operator $o$ and a symbol $u$, $o[u]$ is an operator.Symbolic parameterjust nowAnalogous to Symbol.Symmetricjust nowA property of a Binary relation $R$ on a set $T$ such that if $t\ R\ s$ then $s\ R\ t$, for every $t$, $s$ $\in T$.Symmetryjust nowNo description yetSyntactic abstractionjust nowA mechanism for defining new syntax forms, typically through Macros, that expand into existing language constructs. Enables language extension without modifying the core implementation.Syntactic categoryjust now(Syntax & Grammar) According to Practical foundations for programming languages, largely analogous with Sort. Roughly means "syntactic type".Syntactic sugarjust nowA more convenient or readable syntax that is transformed into a Core calculus/language construct, providing expressiveness without extending the language's fundamental semantics.Syntax tokenjust nowNo description yetSyntax treejust nowNo description yetSystemjust nowPapers: On the Criteria To Be Used in Decomposing Systems into Modules (../../Papers/Papers/On%20the%20Criteria%20To%20Be%20Used%20in%20Decomposing%20Systems%20%2031baa8fcd08880429536c92add4ffb42.md)T45
Tacticjust nowTools: Rocq (formerly Coq)Tactic modifierjust nowTools: Rocq (formerly Coq)Tagged unionjust nowSynonym for Sum type - "union" because it combines variants, "tagged" because each variant has an explicit Constructor tag distinguishing it (unlike untagged Union type types).Target languagejust nowThe language the compiled program is in.Termjust nowA term is a syntactic phrase in a grammar that represents computation and evaluates to a value - unlike Expression which broadly encompasses any well-formed syntactic construct including types, patterns, and declarations.Term expressionjust nowNo description yetTerm valuejust nowLambda abstractions/Functions are the only values.The diamond problemjust nowAn ambiguity that arises in Multiple inheritance when a class inherits from two classes that both inherit from a common ancestor, causing uncertainty about which inherited member to use.The plait programming languagejust nowA dialect of Lisp, based on Racket, but with Type system resembling that of ML.Tokenjust nowNo description yetTop down constructionjust nowSynonymous with Backward chaining.Total functionjust nowA Partial function that is defined on all values of its domain.Traitjust nowThis is different from Rust's trait!Trait mixinjust nowNote: Trait in this sense is different from Rust’s traits.Transition functionjust nowA Partial function from machine configurations (term, environment, stack, etc.) to successor configurations, defining each atomic step of execution until a final state is reached. In Lambda calculus with Small-step/Structural operational semantics (SOS), the transition function usually relates a term with a simplification of that term, and is undefined for Normal forms.Transitivejust nowA property of a Binary relation $R$ on a set $T$ such that if $t 0\ R\ t 1$ and $t 1\ R\ t 2$ then $t 0\ R\ t 2$, for every $t 0$, $t 1$, $t 2$ $\in T$.Transitive closurejust nowA smallest superset of a set that is Transitive.Transitivityjust nowNo description yetTrapped runtime errorjust nowAccording to "Type system" [Luca Cardelli, 1996], a type of errors that immediately terminate the program, such as division by zero, array index out-of-bound (in Java, Rust, etc.). These are deemed as safe as they cannot corrupt the program's state.Trapped runtime error untrapped runtime errorjust nowAccording to "Type system" [Luca Cardelli, 1996], a type of errors that immediately terminate the program, such as division by zero, array index out-of-bound (in Java, Rust, etc.). These are deemed as safe as they cannot corrupt the program's state.Tree agnostic parserjust nowNo description yetTree inductionjust nowFormally, assume $a\ \text{tree}$ means that $a$ is a binary tree. To prove that whenever $a\ \text{tree}$, we have $\mathcal{P}(a)$, it's sufficient to show that:Truthyjust nowA value that evaluates as true in a boolean context despite not being literally true (like non-zero numbers or non-empty strings in dynamic languages).Truthy falsy conditional expressionjust nowNo description yetTuplejust nowA data structure that groups a fixed number of values of possibly different types (like (1, \"hello\", true)), accessed by position rather than name.Tuple rocqjust nowMultiple fields inside a constructor.Turbofishjust nowNo description yetType annotationjust nowA syntactic hint to the Type checker declaring the intended type of a term, used to guide inference, resolve ambiguity, or make types explicit for documentation.Type ascriptionjust nowNo description yetType checkerjust nowA program or algorithm that verifies type correctness by analyzing program text and ensuring expressions conform to typing rules before execution.Type compatibilityjust nowA relation between types that implies Substitutability. A static approximation of Substitutability.Type constructorjust nowA function at the type level that builds new types from existing ones, such as List, Array, or the arrow constructor ($\\to$) that constructs function types.Type environmentjust nowA mapping from variable names to their types, often written as $\Gamma$, that tracks type bindings in scope during Type checker analysis, extended when entering new binding forms.Type errorjust nowAccording to Programming languages: Application and Interpretation, an inability to construct a proof that a given term has some consistent type.Type inferencejust nowThe automatic deduction of types from program context without explicit annotations, using constraint solving or unification algorithms (e.g., Hindley-Milner system) to determine (usually) the most general types.Type narrowingjust nowAnalogy: Think of types as sets, then type narrowing means to narrow a set (Supertype -> Subtype).Type predicatejust nowA function that tests whether a value belongs to a specific type and informs the Type checker of this fact - enables Type narrowing after the check (e.g., mt?, string?, typeof).Type safetyjust now(Type theory, Language feature/design, Semantics) According to Robert (Bob) Harper, the coherence between Static semantics and Dynamic semantics.Type safety language safetyjust nowThe property of a language in which every well-typed program (accepted by the static semantics typing rules) will never reach a “stuck term” state due to misusing values according to their types.Type systemjust nowA tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.Type theoryjust nowA Formal system where every term has a type, providing a foundation for mathematics and programming through the Curry-Howard correspondence between proofs and programs.Type variablejust nowA placeholder (e.g., $T$, $U$, $\\alpha$) representing an unknown or generic type - gets instantiated to a concrete type during type checking or remains polymorphic.Type variantjust nowA variant of a Sum type.Type wideningjust nowAnalogy: Think of types as sets, then type widening means to widen a set (Subtype -> Supertype).Typing judgmentjust nowA formal statement asserting that a term has a particular type under a given Type environment, typically written as $\Gamma \vdash t : T$.U11
Unfoldjust nowA reduction step that replaces a defined name with its definition body, expanding abbreviations to expose underlying structure.Uniformjust nowNo description yetUniformityjust nowNo description yetUnion typejust nowUnion type: An untagged, ad-hoc combination of existing independent types (e.g., (U mt node)) - unlike Sum type (Algebraic data type) where Type variant are tagged and defined together as part of oneUnion type retrofitted type systemjust nowNo description yetUniversalityjust nowNo description yetUntitledjust nowNo description yetUntrapped runtime errorjust nowAccording to "Type system" [Luca Cardelli, 1996], a type of errors that does not terminate the program, such as buffer overflows, accessing deallocated memory, type punning gone wrong. These are deemed as dangerous as they can corrupt the program's state.Untyped calculus of booleans and numbersjust now$$Untyped calculus of booleans and numbers nonsensical termjust now$$Unwrapjust nowAn operation that extracts inner values from a wrapper type via Pattern matching (like getting x from Some x), exposing the contained data for use.V13
Valencejust nowThe specification of how many variables a subterm binds and what Sorts (types) those variables have.Valence actual parameter argumentjust nowNo description yetValidityjust nowNo description yetValuejust nowA Term in Normal form that is not deemed a bad state.Value environmentjust nowA mapping from variable names to runtime values used during interpretation.Variablejust now(Syntax & Grammar) According to Practical foundations for programming languages , specifically Chapter 1. Abstract syntax, a syntactic variable which is a placeholder for an Abstract syntax tree (AST) of a specific Sort.Variable abstract syntax tree astjust nowNo description yetVariable capturejust nowExample:Variable definitionjust nowA syntactic construct that introduces a new variable name and establishes a binding - optionally with an initial value (e.g., let x = 5).Variadic treejust nowA tree structure where operators can take a variable (not fixed) number of arguments, with that number determined by a Symbol index.Vectorjust nowA contiguous, dynamically-sized array data structure supporting indexed access and operations like append, typically allocated on the Heap.Visibilityjust nowOwner: Huy Đỗ Nguyễn AnCategory: Book walkthrough, RubyParent wiki page: Ruby foundations (../Ruby%20foundations%2054af0db86b8a443b8ab70622d1aa508b.md)Visiblejust nowBooks & Chapters: Chapter 1 - The Psychopathology of Everyday Things (../../Books/Books%20&%20Chapters/Chapter%201%20-%20The%20Psychopathology%20of%20Everyday%20Things%202e8aa8fcd08880ab9bfaf8cd47f3634a.md)W5
Weakeningjust nowNo description yetWell foundedjust nowThe property of a Preorder whose strict part ($a < b \iff a \le b\land b \not\le a$ ) admits no infinite descending chains, ensuring every non-empty subset has a minimal element.Wildcard patternjust nowA Pattern (usually written ` `) that matches any value without binding it to a name, useful for ignoring irrelevant cases in Pattern matching.Wildcard pattern rocqjust nowA Pattern (usually written ` `) that matches any value without binding it to a name, useful for ignoring irrelevant cases in Pattern matching.Witnessjust nowA specific object that satisfies an existential claim, for example, a concrete value $t$ for $\exists x., P(x)$ such that $P(t)$ holds.