Scholarly index
Definitions
- Definition 1.1 — Judgment forms and judgmentsJudgments, Derivations, and Operational Semantics
- Definition 1.2 — RuleJudgments, Derivations, and Operational Semantics
- Definition 1.4 — Inductive definitionJudgments, Derivations, and Operational Semantics
- Definition 1.11 — DerivationJudgments, Derivations, and Operational Semantics
- Definition 1.20 — Iterated inductive definitionJudgments, Derivations, and Operational Semantics
- Definition 1.22 — Simultaneous definitionJudgments, Derivations, and Operational Semantics
- Definition 1.30 — Hypothetical derivabilityJudgments, Derivations, and Operational Semantics
- Definition 1.32 — Derivable and admissible rulesJudgments, Derivations, and Operational Semantics
- Definition 1.36 — Arithmetic expressions and numeralsJudgments, Derivations, and Operational Semantics
- Definition 1.38 — Small-step arithmetic evaluationJudgments, Derivations, and Operational Semantics
- Definition 1.41 — Many stepsJudgments, Derivations, and Operational Semantics
- Definition 1.43 — Big-step arithmetic evaluationJudgments, Derivations, and Operational Semantics
- Definition 1.50 — Raw untyped termsJudgments, Derivations, and Operational Semantics
- Definition 1.51 — Fresh renamingJudgments, Derivations, and Operational Semantics
- Definition 1.53 — Alpha-equivalenceJudgments, Derivations, and Operational Semantics
- Definition 1.59 — Fresh renaming of quotient termsJudgments, Derivations, and Operational Semantics
- Definition 1.58 — Capture-avoiding substitutionJudgments, Derivations, and Operational Semantics
- Definition 1.64 — Raw values and raw numeric valuesJudgments, Derivations, and Operational Semantics
- Definition 1.65 — Raw call-by-value rule instancesJudgments, Derivations, and Operational Semantics
- Definition 1.61 — Values and numeric valuesJudgments, Derivations, and Operational Semantics
- Definition 1.63 — Call-by-value closureJudgments, Derivations, and Operational Semantics
- Definition 1.67 — Evaluation contexts and contractionsJudgments, Derivations, and Operational Semantics
- Definition 1.68 — Stuck termJudgments, Derivations, and Operational Semantics
- Definition 1.71 — Big-step evaluationJudgments, Derivations, and Operational Semantics
- Definition 2.1 — Simple typesSimple Types, Curry–Howard, Safety, and Normalization
- Definition 2.2 — Raw termsSimple Types, Curry–Howard, Safety, and Normalization
- Definition 2.4 — ContextsSimple Types, Curry–Howard, Safety, and Normalization
- Definition 2.5 — TypingSimple Types, Curry–Howard, Safety, and Normalization
- Definition 2.21 — Values and one-step evaluationSimple Types, Curry–Howard, Safety, and Normalization
- Definition 2.26 — The propositional extensionSimple Types, Curry–Howard, Safety, and Normalization
- Definition 2.28 — Sum typesSimple Types, Curry–Howard, Safety, and Normalization
- Definition 2.30 — UnitSimple Types, Curry–Howard, Safety, and Normalization
- Definition 2.31 — VoidSimple Types, Curry–Howard, Safety, and Normalization
- Definition 2.32 — Injection-free termsSimple Types, Curry–Howard, Safety, and Normalization
- Definition 2.30 — Extended values and computationSimple Types, Curry–Howard, Safety, and Normalization
- Definition 2.32 — Call-by-nameSimple Types, Curry–Howard, Safety, and Normalization
- Definition 2.38 — Intuitionistic propositional natural deductionSimple Types, Curry–Howard, Safety, and Normalization
- Definition 2.36 — Compatible proof reductionSimple Types, Curry–Howard, Safety, and Normalization
- Definition 2.38 — Strong normalization and neutral termsSimple Types, Curry–Howard, Safety, and Normalization
- Definition 2.39 — Reducible termsSimple Types, Curry–Howard, Safety, and Normalization
- Definition 2.41 — Reducible substitutionSimple Types, Curry–Howard, Safety, and Normalization
- Definition 3.1 — First-order syntaxFirst-Order Proof Theory and Sequent Calculi
- Definition 3.4 — First-order natural deductionFirst-Order Proof Theory and Sequent Calculi
- Definition 3.5 — First-order interpretationsFirst-Order Proof Theory and Sequent Calculi
- Definition 3.12 — LJFirst-Order Proof Theory and Sequent Calculi
- Definition 3.19 — MulticutFirst-Order Proof Theory and Sequent Calculi
- Definition 3.24 — Cut measureFirst-Order Proof Theory and Sequent Calculi
- Definition 3.30 — Compatible proof reductionFirst-Order Proof Theory and Sequent Calculi
- Definition 3.35 — Bounded LJ searchFirst-Order Proof Theory and Sequent Calculi
- Definition 3.1 — Terms of the let-languageHindley–Milner Type Inference
- Definition 3.4 — Type variables and monotypesHindley–Milner Type Inference
- Definition 3.5 — SubstitutionsHindley–Milner Type Inference
- Definition 3.6 — Type schemesHindley–Milner Type Inference
- Definition 3.7 — ContextsHindley–Milner Type Inference
- Definition 3.8 — InstancesHindley–Milner Type Inference
- Definition 3.12 — GeneralizationHindley–Milner Type Inference
- Definition 3.16 — TypingHindley–Milner Type Inference
- Definition 4.22 — Pure call-by-value dynamicsHindley–Milner Type Inference
- Definition 4.23 — Constraint generationHindley–Milner Type Inference
- Definition 3.20 — Equation problems and unifiersHindley–Milner Type Inference
- Definition 3.22 — The unification algorithmHindley–Milner Type Inference
- Definition 3.27 — Fresh instantiationHindley–Milner Type Inference
- Definition 3.28 — Algorithm WHindley–Milner Type Inference
- Definition 4.34 — Legal fresh supplyHindley–Milner Type Inference
- Definition 3.31 — Syntax-directed HM typingHindley–Milner Type Inference
- Definition 4.50 — HM evidence core and erasureHindley–Milner Type Inference
- Definition 4.51 — Evidence checkingHindley–Milner Type Inference
- Definition 4.55 — List syntax and typingHindley–Milner Type Inference
- Definition 4.56 — List constructor clauses of WHindley–Milner Type Inference
- Definition 4.57 — List case clause of WHindley–Milner Type Inference
- Definition 4.60 — List contractionsHindley–Milner Type Inference
- Definition 4.61 — Reference roots for the counterexampleHindley–Milner Type Inference
- Definition 4.62 — Reference and cumulative signaturesHindley–Milner Type Inference
- Definition 3.39 — Conservative value restrictionHindley–Milner Type Inference
- Definition 4.68 — Run-time typing over a storeHindley–Milner Type Inference
- Definition 5.1 — MatchingSemi-Unification and Polymorphic Recursion
- Definition 5.2 — Semi-unification problemSemi-Unification and Polymorphic Recursion
- Definition 5.5 — Milner–Mycroft typingSemi-Unification and Polymorphic Recursion
- Definition 5.6 — First-order Milner–Mycroft templatesSemi-Unification and Polymorphic Recursion
- Definition 5.7 — Syntax-directed MM presentationSemi-Unification and Polymorphic Recursion
- Definition 5.11 — Generated constraint problemSemi-Unification and Polymorphic Recursion
- Definition 5.13 — Encodings and log-space reductionSemi-Unification and Polymorphic Recursion
- Definition 5.20 — Computability interfaceSemi-Unification and Polymorphic Recursion
- Definition 5.29 — Fixed-annotation checkingSemi-Unification and Polymorphic Recursion
- Definition 6.1 — Dimension expressionDimension Types and Units of Measure
- Definition 6.3 — Units and scalesDimension Types and Units of Measure
- Definition 6.4 — Types, schemes, and termsDimension Types and Units of Measure
- Definition 6.5 — Dimension typingDimension Types and Units of Measure
- Definition 6.6 — Syntax-directed dimension typingDimension Types and Units of Measure
- Definition 6.12 — Principal dimension solverDimension Types and Units of Measure
- Definition 6.16 — Dimension-aware inferenceDimension Types and Units of Measure
- Definition 6.22 — Canonical numeric coreDimension Types and Units of Measure
- Definition 6.23 — Core typingDimension Types and Units of Measure
- Definition 6.24 — Core dynamicsDimension Types and Units of Measure
- Definition 6.30 — Coherent scale changeDimension Types and Units of Measure
- Definition 4.1 — Types, rows, and lacks predicatesRow Polymorphism and Extensible Records and Variants
- Definition 4.2 — Constraint entailment and strict formationRow Polymorphism and Extensible Records and Variants
- Definition 7.3 — Admissible substitutionRow Polymorphism and Extensible Records and Variants
- Definition 7.4 — Strict formationRow Polymorphism and Extensible Records and Variants
- Definition 4.3 — Row equalityRow Polymorphism and Extensible Records and Variants
- Definition 4.6 — Qualified schemesRow Polymorphism and Extensible Records and Variants
- Definition 4.7 — Qualified typingRow Polymorphism and Extensible Records and Variants
- Definition 4.13 — Record terms and typingRow Polymorphism and Extensible Records and Variants
- Definition 4.8 — Substitution and qualified-context equivalenceRow Polymorphism and Extensible Records and Variants
- Definition 4.15 — Variant terms and typingRow Polymorphism and Extensible Records and Variants
- Definition 4.17 — Values, contexts, and primitive reductionRow Polymorphism and Extensible Records and Variants
- Definition 4.23 — Constrained insertion and unificationRow Polymorphism and Extensible Records and Variants
- Definition 7.31 — Finite-multiset descentRow Polymorphism and Extensible Records and Variants
- Definition 4.29 — Qualified Algorithm WRow Polymorphism and Extensible Records and Variants
- Definition 4.32 — Regular output of row inferenceRow Polymorphism and Extensible Records and Variants
- Definition 4.36 — Evidence for lacksRow Polymorphism and Extensible Records and Variants
- Definition 4.38 — Evidence-passing target calculusRow Polymorphism and Extensible Records and Variants
- Definition 7.50 — Target row primitivesRow Polymorphism and Extensible Records and Variants
- Definition 7.51 — Target dynamics and canonical valuesRow Polymorphism and Extensible Records and Variants
- Definition 4.39 — Canonical offset representationRow Polymorphism and Extensible Records and Variants
- Definition 7.53 — Unambiguous evidence interfaceRow Polymorphism and Extensible Records and Variants
- Definition 4.40 — Evidence elaborationRow Polymorphism and Extensible Records and Variants
- Definition 4.42 — Ground value relationRow Polymorphism and Extensible Records and Variants
- Definition 8.1 — Formation, kind assignment, and record kindType-Preserving Compilation of Polymorphic Records
- Definition 8.2 — Kind-respecting substitutionType-Preserving Compilation of Polymorphic Records
- Definition 8.6 — Source typingType-Preserving Compilation of Polymorphic Records
- Definition 8.7 — Target types and kindsType-Preserving Compilation of Polymorphic Records
- Definition 8.8 — Index assignmentsType-Preserving Compilation of Polymorphic Records
- Definition 8.9 — Ground numeral substitutionType-Preserving Compilation of Polymorphic Records
- Definition 8.11 — Target term typingType-Preserving Compilation of Polymorphic Records
- Definition 8.14 — CompilationType-Preserving Compilation of Polymorphic Records
- Definition 8.18 — Closing logical relationType-Preserving Compilation of Polymorphic Records
- Definition 5.1 — Types and annotated termsSystem F, Impredicativity, and Normalization
- Definition 5.3 — ContextsSystem F, Impredicativity, and Normalization
- Definition 5.4 — Type formation and Church typingSystem F, Impredicativity, and Normalization
- Definition 5.8 — Call-by-value reductionSystem F, Impredicativity, and Normalization
- Definition 5.13 — Compatible beta reductionSystem F, Impredicativity, and Normalization
- Definition 5.15 — Church booleansSystem F, Impredicativity, and Normalization
- Definition 5.16 — Church productsSystem F, Impredicativity, and Normalization
- Definition 5.17 — Church sumsSystem F, Impredicativity, and Normalization
- Definition 5.18 — Church natural numbersSystem F, Impredicativity, and Normalization
- Definition 5.19 — Curry-style System FSystem F, Impredicativity, and Normalization
- Definition 5.20 — ErasureSystem F, Impredicativity, and Normalization
- Definition 5.24 — Strong normalization and neutral termsSystem F, Impredicativity, and Normalization
- Definition 5.25 — Reducibility candidateSystem F, Impredicativity, and Normalization
- Definition 5.27 — Candidate valuation and type interpretationSystem F, Impredicativity, and Normalization
- Definition 5.33 — Reducible term substitutionSystem F, Impredicativity, and Normalization
- Definition 9.40 — Parallel beta reductionSystem F, Impredicativity, and Normalization
- Definition 9.47 — Full-function interpretation packageSystem F, Impredicativity, and Normalization
- Definition 9.48 — T-algebras and splittingSystem F, Impredicativity, and Normalization
- Definition 5.42 — Lifting a relation through an arrowSystem F, Impredicativity, and Normalization
- Definition 6.1 — Closed terms modulo betaRelational Parametricity and Abstraction Theorems
- Definition 6.2 — Arrow lifting and graphsRelational Parametricity and Abstraction Theorems
- Definition 6.4 — Relation environmentsRelational Parametricity and Abstraction Theorems
- Definition 6.5 — Relational interpretation of typesRelational Parametricity and Abstraction Theorems
- Definition 10.7 — Logical relationRelational Parametricity and Abstraction Theorems
- Definition 6.9 — Related closing substitutionsRelational Parametricity and Abstraction Theorems
- Definition 10.22 — Strict admissible relationRelational Parametricity and Abstraction Theorems
- Definition 10.24 — Logic-of-parametricity comparison interfaceRelational Parametricity and Abstraction Theorems
- Definition 10.25 — Effectful PE comparison interfaceRelational Parametricity and Abstraction Theorems
- Definition 7.1 — KindsType Operators, Kinds, and System F-omega
- Definition 7.2 — Constructors of F_ωType Operators, Kinds, and System F-omega
- Definition 7.4 — Type-level reductionType Operators, Kinds, and System F-omega
- Definition 7.5 — Constructor equalityType Operators, Kinds, and System F-omega
- Definition 7.6 — Terms and typing of F_ωType Operators, Kinds, and System F-omega
- Definition 11.7 — Pure call-by-value evaluationType Operators, Kinds, and System F-omega
- Definition 7.13 — Strong normalizationType Operators, Kinds, and System F-omega
- Definition 7.15 — ReducibilityType Operators, Kinds, and System F-omega
- Definition 11.30 — Deterministic constructor normalizationType Operators, Kinds, and System F-omega
- Definition 11.41 — Syntax-directed term inferenceType Operators, Kinds, and System F-omega
- Definition 7.31 — Existential package terms and typingExistential Types, Abstract Data, and Representation Independence
- Definition 7.32 — The abstract counter interfaceExistential Types, Abstract Data, and Representation Independence
- Definition 7.34 — Call-by-value evaluation with packagesExistential Types, Abstract Data, and Representation Independence
- Definition 7.35 — Compatible term beta conversionExistential Types, Abstract Data, and Representation Independence
- Definition 7.41 — Relations at a kindExistential Types, Abstract Data, and Representation Independence
- Definition 7.42 — Higher-kinded environmentsExistential Types, Abstract Data, and Representation Independence
- Definition 7.43 — Relational interpretation of constructorsExistential Types, Abstract Data, and Representation Independence
- Definition 13.1 — Resolution selectors and evidence storesQualified Types, Type Classes, and Coherent Dictionary Elaboration
- Definition 13.3 — Canonical predicate normalizationQualified Types, Type Classes, and Coherent Dictionary Elaboration
- Definition 13.4 — Replay of a normalization traceQualified Types, Type Classes, and Coherent Dictionary Elaboration
- Definition 13.5 — Ground solvability and equivalenceQualified Types, Type Classes, and Coherent Dictionary Elaboration
- Definition 13.14 — Evidence targetQualified Types, Type Classes, and Coherent Dictionary Elaboration
- Definition 13.22 — Inference with pending equality constraintsQualified Types, Type Classes, and Coherent Dictionary Elaboration
- Definition 12.1 — SignaturesML Modules: Abstraction, Functors, and Sharing
- Definition 12.2 — Modules and projectible valuesML Modules: Abstraction, Functors, and Sharing
- Definition 14.6 — Algorithmic signature matchingML Modules: Abstraction, Functors, and Sharing
- Definition 14.9 — Hereditary module substitutionML Modules: Abstraction, Functors, and Sharing
- Definition 12.5 — Closed package targetML Modules: Abstraction, Functors, and Sharing
- Definition 12.6 — Matching coercionML Modules: Abstraction, Functors, and Sharing
- Definition 14.12 — Elaboration-admissible derivationML Modules: Abstraction, Functors, and Sharing
- Definition 14.13 — Package opening and open translation contextsML Modules: Abstraction, Functors, and Sharing
- Definition 14.14 — Projectible views and derivation-indexed elaborationML Modules: Abstraction, Functors, and Sharing
- Definition 14.20 — Counter representation relationML Modules: Abstraction, Functors, and Sharing
- Definition 12.9 — Counter clientsML Modules: Abstraction, Functors, and Sharing
- Definition 14.22 — Value and computation relations for counter clientsML Modules: Abstraction, Functors, and Sharing
- Definition 12.12 — Principal signature of a projectible valueML Modules: Abstraction, Functors, and Sharing
- Definition 15.1 — The finite linking calculus Mix_0MixML, Recursive Linking, and Definedness
- Definition 15.2 — Compatible signaturesMixML, Recursive Linking, and Definedness
- Definition 15.3 — Initialization judgmentMixML, Recursive Linking, and Definedness
- Definition 15.6 — Ordered slot commands and extracted tracesMixML, Recursive Linking, and Definedness
- Definition 15.7 — Trace validationMixML, Recursive Linking, and Definedness
- Definition 15.9 — The load-bearing LTG store interfaceMixML, Recursive Linking, and Definedness
- Definition 15.10 — Full MixML semantic-signature shellMixML, Recursive Linking, and Definedness
- Definition 15.11 — Three-pass interfaceMixML, Recursive Linking, and Definedness
- Definition 16.1 — Atomic class signatureModular Type Classes and Implicit Modules
- Definition 16.2 — The finite calculus MTC_0Modular Type Classes and Implicit Modules
- Definition 16.3 — Explicit adoptionModular Type Classes and Implicit Modules
- Definition 16.5 — Deterministic resolverModular Type Classes and Implicit Modules
- Definition 16.10 — Constraint reduction in the finite sliceModular Type Classes and Implicit Modules
- Definition 16.12 — System card for modular type classesModular Type Classes and Implicit Modules
- Definition 16.15 — Resolution discipline of modular implicitsModular Type Classes and Implicit Modules
- Definition 16.16 — Well-scoped SI derivationModular Type Classes and Implicit Modules
- Definition 7.58 — Shallow prequotationTyped Self-Representation in System F-omega
- Definition 7.62 — Deep prequotation and quotationTyped Self-Representation in System F-omega
- Definition 7.72 — Neutral and normal termsTyped Self-Representation in System F-omega
- Definition 8.1 — The first-order subtype calculusSubtyping, Records, and Bounded Quantification
- Definition 8.4 — Intrinsic and coercive readingsSubtyping, Records, and Bounded Quantification
- Definition 8.13 — Join and meetSubtyping, Records, and Bounded Quantification
- Definition 18.17 — Recursive boundsSubtyping, Records, and Bounded Quantification
- Definition 8.15 — Kernel F_<: over the record coreSubtyping, Records, and Bounded Quantification
- Definition 8.17 — Formation of mixed contextsSubtyping, Records, and Bounded Quantification
- Definition 8.28 — Closed full-F_<: statementsSubtyping, Records, and Bounded Quantification
- Definition 18.38 — The two machine models in the importSubtyping, Records, and Bounded Quantification
- Definition 19.1 — The frozen MLsub fragment MLsub_0Algebraic Subtyping and Principal Inference
- Definition 19.2 — Algebraic subtype lawsAlgebraic Subtyping and Principal Inference
- Definition 19.3 — Lambda-lifted declarative typingAlgebraic Subtyping and Principal Inference
- Definition 19.4 — BisubstitutionAlgebraic Subtyping and Principal Inference
- Definition 19.5 — Atomic eliminationAlgebraic Subtyping and Principal Inference
- Definition 19.8 — Biunification work listAlgebraic Subtyping and Principal Inference
- Definition 19.10 — Finite polar type automataAlgebraic Subtyping and Principal Inference
- Definition 19.12 — Polar inferenceAlgebraic Subtyping and Principal Inference
- Definition 19.15 — Boolean-algebraic comparison signatureAlgebraic Subtyping and Principal Inference
- Definition 9.4 — Finite types and atomsIntersection, Union, and Semantic Subtyping
- Definition 9.1 — Interface, intersection, and application rulesIntersection, Union, and Semantic Subtyping
- Definition 9.5 — Universal finite-graph domainIntersection, Union, and Semantic Subtyping
- Definition 9.6 — InterpretationIntersection, Union, and Semantic Subtyping
- Definition 9.9 — Disjunctive normal formIntersection, Union, and Semantic Subtyping
- Definition 9.13 — Finite simulationsIntersection, Union, and Semantic Subtyping
- Definition 9.18 — Test types, terms, and admissible interfacesIntersection, Union, and Semantic Subtyping
- Definition 9.19 — Structural testIntersection, Union, and Semantic Subtyping
- Definition 9.20 — Weak call-by-value reductionIntersection, Union, and Semantic Subtyping
- Definition 9.22 — Least application outputIntersection, Union, and Semantic Subtyping
- Definition 9.24 — Least projection outputsIntersection, Union, and Semantic Subtyping
- Definition 9.26 — Declarative typingIntersection, Union, and Semantic Subtyping
- Definition 9.28 — Exact introduction type of a valueIntersection, Union, and Semantic Subtyping
- Definition 9.34 — SynthesisIntersection, Union, and Semantic Subtyping
- Definition 21.1 — The top-free merge calculusDisjoint Intersections, Merge Elaboration, and Coherence
- Definition 21.2 — Coercive subtypingDisjoint Intersections, Merge Elaboration, and Coherence
- Definition 21.4 — Simple disjointness and well-formed typesDisjoint Intersections, Merge Elaboration, and Coherence
- Definition 21.6 — Algorithmic disjointnessDisjoint Intersections, Merge Elaboration, and Coherence
- Definition 21.9 — Elaborating bidirectional typingDisjoint Intersections, Merge Elaboration, and Coherence
- Definition 10.1 — Source calculus, bind composition, and reductionRefinement Types and Proof-Carrying Programs
- Definition 22.2 — Bind compositionRefinement Types and Proof-Carrying Programs
- Definition 22.3 — ReductionRefinement Types and Proof-Carrying Programs
- Definition 10.3 — Difference predicates, refinement types, and substitutionRefinement Types and Proof-Carrying Programs
- Definition 10.4 — Scopes, well-formed contexts, and typesRefinement Types and Proof-Carrying Programs
- Definition 10.5 — Context embedding and entailmentRefinement Types and Proof-Carrying Programs
- Definition 10.6 — Constraint graph and replay certificatesRefinement Types and Proof-Carrying Programs
- Definition 10.6 — Constraint graph and replay certificatesRefinement Types and Proof-Carrying Programs
- Definition 10.11 — Declarative subtypingRefinement Types and Proof-Carrying Programs
- Definition 10.14 — Exact base types and declarative typingRefinement Types and Proof-Carrying Programs
- Definition 10.15 — VC generationRefinement Types and Proof-Carrying Programs
- Definition 10.27 — Finite qualifier templates and enumerationRefinement Types and Proof-Carrying Programs
- Definition 10.29 — First-order guard elaborationRefinement Types and Proof-Carrying Programs
- Definition 10.31 — Source proof-carrying-code protocolRefinement Types and Proof-Carrying Programs
- Definition 10.33 — Simply typed erasure targetRefinement Types and Proof-Carrying Programs
- Definition 23.1 — The gradual source calculusGradual Typing and the Dynamic Boundary
- Definition 23.5 — Ground types, casts, and target typingGradual Typing and the Dynamic Boundary
- Definition 23.6 — Call-by-value reductionGradual Typing and the Dynamic Boundary
- Definition 23.8 — Cast insertionGradual Typing and the Dynamic Boundary
- Definition 23.17 — Positive and negative safetyGradual Typing and the Dynamic Boundary
- Definition 23.21 — Label safetyGradual Typing and the Dynamic Boundary
- Definition 23.26 — Type, context, and source-term precisionGradual Typing and the Dynamic Boundary
- Definition 23.30 — Typed target precisionGradual Typing and the Dynamic Boundary
- Definition 23.34 — Related closing substitutionsGradual Typing and the Dynamic Boundary
- Definition 23.36 — Related evaluation framesGradual Typing and the Dynamic Boundary
- Definition 23.41 — Stutter measureGradual Typing and the Dynamic Boundary
- Definition 23.45 — DivergenceGradual Typing and the Dynamic Boundary
- Definition 23.49 — Executable boundary contractsGradual Typing and the Dynamic Boundary
- Definition 23.53 — The SD source/target cardGradual Typing and the Dynamic Boundary
- Definition 24.1 — The eager iso-recursive calculusRecursive Types, Domains, and General Recursion
- Definition 24.6 — Contractive regular types and tree equalityRecursive Types, Domains, and General Recursion
- Definition 24.7 — Worklist equality algorithmRecursive Types, Domains, and General Recursion
- Definition 24.10 — Call-by-name PCFRecursive Types, Domains, and General Recursion
- Definition 24.13 — Pointed omega-cpos and continuityRecursive Types, Domains, and General Recursion
- Definition 24.23 — The partial-list orderRecursive Types, Domains, and General Recursion
- Definition 24.30 — Strict natural operationsRecursive Types, Domains, and General Recursion
- Definition 24.32 — PCF denotationRecursive Types, Domains, and General Recursion
- Definition 24.35 — Logical approximationRecursive Types, Domains, and General Recursion
- Definition 24.41 — Step-indexed equivalenceRecursive Types, Domains, and General Recursion
- Definition 24.48 — An eta-delayed call-by-value fixed pointRecursive Types, Domains, and General Recursion
- Definition 24.52 — Finite tail observationRecursive Types, Domains, and General Recursion
- Definition 24.53 — Safety, correctness, termination, productivity, totalityRecursive Types, Domains, and General Recursion
- Definition 24.55 — The unrestricted proof-recursion extensionRecursive Types, Domains, and General Recursion
- Definition 15.1 — The functional object calculus Ob_1Object Calculi and Recursive Object Types
- Definition 15.2 — Weak object reductionObject Calculi and Recursive Object Types
- Definition 15.6 — Width-invariant object subtypingObject Calculi and Recursive Object Types
- Definition 15.7 — Syntax-directed minimum typingObject Calculi and Recursive Object Types
- Definition 15.13 — The recursive moving-point typeObject Calculi and Recursive Object Types
- Definition 15.16 — The target calculus F_<:μObject Calculi and Recursive Object Types
- Definition 15.17 — Target reductionObject Calculi and Recursive Object Types
- Definition 26.1 — The corrected row-expression fragmentCorrected Inference for Simple Objects
- Definition 26.4 — Presence obligationsCorrected Inference for Simple Objects
- Definition 16.4 — The calculus Self_+OO Self Types, F-Bounds, and Matching
- Definition 16.5 — Call-by-value reductionOO Self Types, F-Bounds, and Matching
- Definition 16.11 — F-bounded quantificationOO Self Types, F-Bounds, and Matching
- Definition 21.13 — Restricted higher-order target H_μOO Self Types, F-Bounds, and Matching
- Definition 16.13 — Higher-order matchingOO Self Types, F-Bounds, and Matching
- Definition 21.20 — Syntactic worlds and closing substitutionsOO Self Types, F-Bounds, and Matching
- Definition 21.21 — Step-indexed interpretationOO Self Types, F-Bounds, and Matching
- Definition 22.1 — Well-founded operation treesEffects, Monads, CBPV, and Algebraic Operations
- Definition 22.2 — Return and bindEffects, Monads, CBPV, and Algebraic Operations
- Definition 22.3 — Monad, in return-and-bind formEffects, Monads, CBPV, and Algebraic Operations
- Definition 22.6 — Effect theory and Kleisli congruenceEffects, Monads, CBPV, and Algebraic Operations
- Definition 22.7 — Handler algebra and foldEffects, Monads, CBPV, and Algebraic Operations
- Definition 22.10 — CBPV_0Effects, Monads, CBPV, and Algebraic Operations
- Definition 22.20 — Annotated typing rulesEffects, Monads, CBPV, and Algebraic Operations
- Definition 22.21 — Annotated handler judgmentEffects, Monads, CBPV, and Algebraic Operations
- Definition 22.28 — First-order reificationEffects, Monads, CBPV, and Algebraic Operations
- Definition 23.1 — Scoped signatureScoped Operations and Explicit Substitution
- Definition 23.2 — Exact nested syntaxScoped Operations and Explicit Substitution
- Definition 23.4 — Reindexing equationScoped Operations and Explicit Substitution
- Definition 23.9 — Explicit substitutionScoped Operations and Explicit Substitution
- Definition 23.17 — Structural continuation translationScoped Operations and Explicit Substitution
- Definition 24.2 — Higher-order effect signatureHigher-Order Algebraic Effects and Modular Elaboration
- Definition 24.3 — Hefty treeHigher-Order Algebraic Effects and Modular Elaboration
- Definition 24.4 — The catch signatureHigher-Order Algebraic Effects and Modular Elaboration
- Definition 24.6 — Hefty bindHigher-Order Algebraic Effects and Modular Elaboration
- Definition 24.9 — Hefty algebraHigher-Order Algebraic Effects and Modular Elaboration
- Definition 24.10 — Hefty catamorphismHigher-Order Algebraic Effects and Modular Elaboration
- Definition 24.12 — ElaborationHigher-Order Algebraic Effects and Modular Elaboration
- Definition 24.14 — Signature-row insertionHigher-Order Algebraic Effects and Modular Elaboration
- Definition 24.16 — Throw handling and maskingHigher-Order Algebraic Effects and Modular Elaboration
- Definition 24.17 — Target free-tree bindHigher-Order Algebraic Effects and Modular Elaboration
- Definition 24.18 — Catch elaborationHigher-Order Algebraic Effects and Modular Elaboration
- Definition 24.22 — Composition of hefty algebrasHigher-Order Algebraic Effects and Modular Elaboration
- Definition 24.25 — State handlingHigher-Order Algebraic Effects and Modular Elaboration
- Definition 25.1 — Effect rows and equivalenceEffect Rows, Principal Type-and-Effect Inference, and Handlers
- Definition 25.3 — Fine-grain effect-row calculusEffect Rows, Principal Type-and-Effect Inference, and Handlers
- Definition 25.4 — Handler typingEffect Rows, Principal Type-and-Effect Inference, and Handlers
- Definition 25.5 — Operational semanticsEffect Rows, Principal Type-and-Effect Inference, and Handlers
- Definition 25.11 — All unification casesEffect Rows, Principal Type-and-Effect Inference, and Handlers
- Definition 25.15 — Algorithm W with effectsEffect Rows, Principal Type-and-Effect Inference, and Handlers
- Definition 31.25 — Internal safetyEffect Rows, Principal Type-and-Effect Inference, and Handlers
- Definition 32.1 — System Xi cardEffect Capabilities and Tunnelling
- Definition 32.2 — Generated configurationEffect Capabilities and Tunnelling
- Definition 32.3 — Undelimited capabilityEffect Capabilities and Tunnelling
- Definition 32.14 — Effekt cardEffect Capabilities and Tunnelling
- Definition 32.17 — Tunnelling calculus cardEffect Capabilities and Tunnelling
- Definition 32.18 — Step-indexed interpretation and closing environmentsEffect Capabilities and Tunnelling
- Definition 32.22 — Program contexts and contextual refinementEffect Capabilities and Tunnelling
- Definition 33.1 — Normal form at an effect contextModal Effect Types and Source-to-Met Encodings
- Definition 34.1 — Name search and identity searchLexical Effect Handlers and Direct Compilation
- Definition 34.2 — The 2024 Lexa system cardLexical Effect Handlers and Direct Compilation
- Definition 34.3 — Lexa configurationsLexical Effect Handlers and Direct Compilation
- Definition 34.5 — The 2024 Salt target cardLexical Effect Handlers and Direct Compilation
- Definition 34.9 — The 2025 SL/TL system cardLexical Effect Handlers and Direct Compilation
- Definition 34.13 — The λ ^ and CPS cardLexical Effect Handlers and Direct Compilation
- Definition 35.1 — The continuation calculus λ _ KControl Operators and Classical Proofs
- Definition 35.7 — Call-by-value CPS typesControl Operators and Classical Proofs
- Definition 35.8 — CPS translation of termsControl Operators and Classical Proofs
- Definition 35.9 — A stack as a target functionControl Operators and Classical Proofs
- Definition 35.18 — The Pir'og–Polesiuk–Sieczkowski (PPS) common coreControl Operators and Classical Proofs
- Definition 35.19 — Deep handlersControl Operators and Classical Proofs
- Definition 35.20 — The parametric shift_0 calculusControl Operators and Classical Proofs
- Definition 35.21 — Deep bridge translationsControl Operators and Classical Proofs
- Definition 35.31 — The shallow pairControl Operators and Classical Proofs
- Definition 35.32 — Shallow bridge translationsControl Operators and Classical Proofs
- Definition 35.41 — The hypothetical commuting-projection calculusControl Operators and Classical Proofs
- Definition 18.1 — Disjoint union of linear contextsLinear and Affine Type Systems
- Definition 18.3 — Types, terms, values, and contextsLinear and Affine Type Systems
- Definition 18.5 — Linear typingLinear and Affine Type Systems
- Definition 18.4 — Root reductionLinear and Affine Type Systems
- Definition 18.7 — File-token dynamicsLinear and Affine Type Systems
- Definition 18.13 — Pathwise free useLinear and Affine Type Systems
- Definition 18.19 — Well-owned file configurationLinear and Affine Type Systems
- Definition 18.23 — Structural deltasLinear and Affine Type Systems
- Definition 36.32 — McBride's rig-indexed cardLinear and Affine Type Systems
- Definition 37.1 — Name and value reductionEvaluation-Strategy Translations
- Definition 37.2 — Linear target reductionEvaluation-Strategy Translations
- Definition 37.7 — Call by letEvaluation-Strategy Translations
- Definition 37.10 — Need and affine targetsEvaluation-Strategy Translations
- Definition 38.1 — Formulas, contexts, and sequentsOrdered and Noncommutative Types and the Lambek Calculus
- Definition 38.2 — The cut-free calculus L_ ordOrdered and Noncommutative Types and the Lambek Calculus
- Definition 38.5 — Cut, height, and formula sizeOrdered and Noncommutative Types and the Lambek Calculus
- Definition 38.10 — Sequent weightOrdered and Noncommutative Types and the Lambek Calculus
- Definition 38.11 — Backward searchOrdered and Noncommutative Types and the Lambek Calculus
- Definition 38.15 — The exact exchange extensionOrdered and Noncommutative Types and the Lambek Calculus
- Definition 39.1 — Unfocused calculusPolarization, Focusing, and Proof Search
- Definition 39.4 — Polarized propositions and erasurePolarization, Focusing, and Proof Search
- Definition 39.6 — Focused sequents and stabilityPolarization, Focusing, and Proof Search
- Definition 39.7 — Suspension-normal syntaxPolarization, Focusing, and Proof Search
- Definition 39.8 — The focused calculusPolarization, Focusing, and Proof Search
- Definition 39.21 — Candidate sequents and saturationPolarization, Focusing, and Proof Search
- Definition 40.1 — The calculus MLL^-Proof Nets, Correctness Criteria, and Cut Elimination
- Definition 40.3 — Cut-free proof structureProof Nets, Correctness Criteria, and Cut Elimination
- Definition 40.4 — TranslationProof Nets, Correctness Criteria, and Cut Elimination
- Definition 40.7 — Danos–Regnier correctnessProof Nets, Correctness Criteria, and Cut Elimination
- Definition 40.10 — Subnet, door, kingdom, and empireProof Nets, Correctness Criteria, and Cut Elimination
- Definition 40.18 — Direct switching checkerProof Nets, Correctness Criteria, and Cut Elimination
- Definition 40.21 — Proof structures with cutsProof Nets, Correctness Criteria, and Cut Elimination
- Definition 40.22 — Local cut reductionProof Nets, Correctness Criteria, and Cut Elimination
- Definition 40.31 — Independent adjacent rulesProof Nets, Correctness Criteria, and Cut Elimination
- Definition 41.1 — Net and interfaceInteraction Nets and Interaction Combinators
- Definition 41.2 — Active pairInteraction Nets and Interaction Combinators
- Definition 41.3 — Interaction systemInteraction Nets and Interaction Combinators
- Definition 41.4 — ReductionInteraction Nets and Interaction Combinators
- Definition 41.6 — Unary addition rulesInteraction Nets and Interaction Combinators
- Definition 41.8 — Strong confluenceInteraction Nets and Interaction Combinators
- Definition 41.11 — DevelopmentInteraction Nets and Interaction Combinators
- Definition 41.13 — Exactly-once lambda termsInteraction Nets and Interaction Combinators
- Definition 42.1 — The opening labeled term graphOptimal Sharing and Graph Reduction
- Definition 42.4 — Diagrammatic translationOptimal Sharing and Graph Reduction
- Definition 42.5 — Access-path readbackOptimal Sharing and Graph Reduction
- Definition 42.7 — Asperti–Mairson cost signatureOptimal Sharing and Graph Reduction
- Definition 43.1 — Formulas and bunchesBunched Implications and Resource Semantics
- Definition 43.2 — One-hole and many-hole bunch contextsBunched Implications and Resource Semantics
- Definition 43.3 — Structural congruenceBunched Implications and Resource Semantics
- Definition 43.5 — The calculus LBI_0Bunched Implications and Resource Semantics
- Definition 43.7 — Formula size and derivation heightBunched Implications and Resource Semantics
- Definition 43.9 — Displayed multicutBunched Implications and Resource Semantics
- Definition 43.12 — Proposed cut ruleBunched Implications and Resource Semantics
- Definition 43.14 — Formula represented by a bunchBunched Implications and Resource Semantics
- Definition 43.16 — Principal cut-free theories and Moore closureBunched Implications and Resource Semantics
- Definition 43.19 — The universal BI algebraBunched Implications and Resource Semantics
- Definition 43.25 — Resource frame and modelBunched Implications and Resource Semantics
- Definition 43.26 — ForcingBunched Implications and Resource Semantics
- Definition 43.28 — Bunch forcing and validityBunched Implications and Resource Semantics
- Definition 43.35 — The elementary term modelBunched Implications and Resource Semantics
- Definition 44.1 — Disjoint heapsSeparation Logic and Local Reasoning
- Definition 44.3 — Heap assertionsSeparation Logic and Local Reasoning
- Definition 44.6 — Command semanticsSeparation Logic and Local Reasoning
- Definition 44.7 — Safety and modified variablesSeparation Logic and Local Reasoning
- Definition 44.10 — Local commandSeparation Logic and Local Reasoning
- Definition 44.12 — Semantic Hoare tripleSeparation Logic and Local Reasoning
- Definition 44.15 — Hoare rulesSeparation Logic and Local Reasoning
- Definition 44.18 — Exact-length chainSeparation Logic and Local Reasoning
- Definition 45.2 — Affine and persistent assertionsConcurrent Separation Logic and Higher-Order Ghost State
- Definition 45.3 — Fancy updates and invariant accessConcurrent Separation Logic and Higher-Order Ghost State
- Definition 45.4 — Authoritative counter resourceConcurrent Separation Logic and Higher-Order Ghost State
- Definition 45.6 — Saved propositionConcurrent Separation Logic and Higher-Order Ghost State
- Definition 45.8 — Logically atomic increment contractConcurrent Separation Logic and Higher-Order Ghost State
- Definition 46.1 — Ownership statesOwnership, Borrowing, and Affine Resource Protocols
- Definition 46.2 — Protocol rulesOwnership, Borrowing, and Affine Resource Protocols
- Definition 46.3 — AgreementOwnership, Borrowing, and Affine Resource Protocols
- Definition 46.8 — Selected Affe bindings and splitOwnership, Borrowing, and Affine Resource Protocols
- Definition 46.10 — Simplified uniqueness coreOwnership, Borrowing, and Affine Resource Protocols
- Definition 46.12 — Pure Borrow formal cardOwnership, Borrowing, and Affine Resource Protocols
- Definition 46.13 — Association and safetyOwnership, Borrowing, and Affine Resource Protocols
- Definition 46.15 — Open Pure Borrow obligationsOwnership, Borrowing, and Affine Resource Protocols
- Definition 47.1 — Rooted term graphUniqueness Types and Destructive Update
- Definition 47.2 — Graph-denotation equalityUniqueness Types and Destructive Update
- Definition 47.3 — Conventional graph typingUniqueness Types and Destructive Update
- Definition 47.6 — Conventional constraint setUniqueness Types and Destructive Update
- Definition 47.9 — Attributed types and correctionUniqueness Types and Destructive Update
- Definition 47.10 — Reference-sensitive graph typingUniqueness Types and Destructive Update
- Definition 47.14 — Attribution problemUniqueness Types and Destructive Update
- Definition 47.18 — Bounded update eligibilityUniqueness Types and Destructive Update
- Definition 48.1 — Overlap and separationPlace Calculi, Partial Moves, and Field-Sensitive Borrowing
- Definition 48.2 — Destructive and nondestructive readsPlace Calculi, Partial Moves, and Field-Sensitive Borrowing
- Definition 48.3 — Borrow exclusionPlace Calculi, Partial Moves, and Field-Sensitive Borrowing
- Definition 48.9 — Linearizable typingPlace Calculi, Partial Moves, and Field-Sensitive Borrowing
- Definition 48.15 — Oxide v4 ownership safetyPlace Calculi, Partial Moves, and Field-Sensitive Borrowing
- Definition 48.16 — Continuation-aware loan collectionPlace Calculi, Partial Moves, and Field-Sensitive Borrowing
- Definition 49.1 — Accessible representationMutable Value Semantics and inout Access
- Definition 49.4 — Book conflict relationMutable Value Semantics and inout Access
- Definition 49.5 — Book exclusivity premiseMutable Value Semantics and inout Access
- Definition 49.8 — Well-formed and well-typed memoryMutable Value Semantics and inout Access
- Definition 50.3 — Satisfiability and closed program statesCapability and Region Types for Typed Memory Management
- Definition 50.9 — L^3 linear-location cardCapability and Region Types for Typed Memory Management
- Definition 50.11 — Linear-region cardCapability and Region Types for Typed Memory Management
- Definition 50.13 — Monadic-region cardCapability and Region Types for Typed Memory Management
- Definition 51.1 — Capture of a typeCapture Types and Capture-Set Polymorphism
- Definition 52.1 — State-indexed handleTypestate and State-Transition Protocols
- Definition 59.1 — Projection and projectabilityMultiparty and Asynchronous Session Types
- Definition 59.2 — Input and output dependenciesMultiparty and Asynchronous Session Types
- Definition 59.3 — Unstuckness and coherenceMultiparty and Asynchronous Session Types
- Definition 59.6 — Pirouette choreographyMultiparty and Asynchronous Session Types
- Definition 60.2 — Pure-type-system specificationThe Lambda Cube and Pure Type Systems
- Definition 60.3 — PTS typingThe Lambda Cube and Pure Type Systems
- Definition 60.5 — Lambda-cube systemsThe Lambda Cube and Pure Type Systems
- Definition 60.9 — Legal PTS expressionsThe Lambda Cube and Pure Type Systems
- Definition 60.25 — Functional and lookup-effective specificationsThe Lambda Cube and Pure Type Systems
- Definition 61.1 — LF typingLogical Frameworks, Encodings, and Adequacy
- Definition 61.2 — Atomic and canonical LF objectsLogical Frameworks, Encodings, and Adequacy
- Definition 61.5 — The implicational LF signatureLogical Frameworks, Encodings, and Adequacy
- Definition 61.8 — Compositionality and adequacyLogical Frameworks, Encodings, and Adequacy
- Definition 61.11 — Intrinsically typed STLC signatureLogical Frameworks, Encodings, and Adequacy
- Definition 61.22 — PHOAS parametricityLogical Frameworks, Encodings, and Adequacy
- Definition 62.1 — Atoms and finite permutationsNominal Syntax, Support, and Binding
- Definition 62.2 — Support, freshness, and equivarianceNominal Syntax, Support, and Binding
- Definition 62.4 — Name abstractionNominal Syntax, Support, and Binding
- Definition 62.8 — Nominal STLC syntaxNominal Syntax, Support, and Binding
- Definition 62.12 — Nominal substitutionNominal Syntax, Support, and Binding
- Definition 62.18 — Typed simultaneous nominal substitutionNominal Syntax, Support, and Binding
- Definition 63.1 — Simply typed contextual modal calculusContextual Modal Type Theory and Beluga
- Definition 63.5 — Dependent contextual canonical formsContextual Modal Type Theory and Beluga
- Definition 63.8 — Paired typing schemaContextual Modal Type Theory and Beluga
- Definition 67.1 — The arithmetic interfaceBar Recursion, Choice, and Program Extraction
- Definition 67.2 — Binary and finite productsBar Recursion, Choice, and Program Extraction
- Definition 67.8 — Simple explicitly controlled productBar Recursion, Choice, and Program Extraction
- Definition 67.11 — Dependent explicitly controlled productBar Recursion, Choice, and Program Extraction
- Definition 67.12 — Restricted Spector recursorBar Recursion, Choice, and Program Extraction
- Definition 68.1 — Collecting transformerAbstract Interpretation, Type Systems, and Verified Static Analysis
- Definition 68.5 — Galois connectionAbstract Interpretation, Type Systems, and Verified Static Analysis
- Definition 68.9 — Structural analyzerAbstract Interpretation, Type Systems, and Verified Static Analysis
- Definition 68.12 — Interval wideningAbstract Interpretation, Type Systems, and Verified Static Analysis
- Definition 68.19 — Constructive Galois connectionAbstract Interpretation, Type Systems, and Verified Static Analysis
- Definition 68.23 — Two soundness targetsAbstract Interpretation, Type Systems, and Verified Static Analysis
- Definition 69.2 — RepresentationSymbolic Execution, Path Conditions, and Concolic Testing
- Definition 70.1 — Low equivalenceInformation-Flow Type Systems and Noninterference
- Definition 26.1 — Binding treesThe Rules of Dependent Type Theory
- Definition 26.3 — Names, size, and raw contextsThe Rules of Dependent Type Theory
- Definition 26.4 — Fresh renamingThe Rules of Dependent Type Theory
- Definition 26.6 — α -equivalenceThe Rules of Dependent Type Theory
- Definition 26.10 — Capture-avoiding substitutionThe Rules of Dependent Type Theory
- Definition 26.13 — The judgment formsThe Rules of Dependent Type Theory
- Definition 26.15 — Contexts and presuppositionsThe Rules of Dependent Type Theory
- Definition 26.16 — Equality rulesThe Rules of Dependent Type Theory
- Definition 26.18 — Conversion of a declarationThe Rules of Dependent Type Theory
- Definition 26.19 — Families and sectionsThe Rules of Dependent Type Theory
- Definition 26.20 — Substitution rulesThe Rules of Dependent Type Theory
- Definition 26.21 — Weakening and the generic elementThe Rules of Dependent Type Theory
- Definition 26.22 — The structural rulesThe Rules of Dependent Type Theory
- Definition 26.35 — Economical presentationThe Rules of Dependent Type Theory
- Definition 26.36 — Structurally stable rule schemesThe Rules of Dependent Type Theory
- Definition 26.45 — Context substitutionThe Rules of Dependent Type Theory
- Definition 27.2 — Rules for ΠDependent Products, Sums, and Unit
- Definition 27.5 — Ordinary functionsDependent Products, Sums, and Unit
- Definition 27.9 — Rules for ΣDependent Products, Sums, and Unit
- Definition 27.14 — Rules forDependent Products, Sums, and Unit
- Definition 27.19 — Term setsDependent Products, Sums, and Unit
- Definition 27.24 — Definitional isomorphismDependent Products, Sums, and Unit
- Definition 28.2 — Rules forInductive Types
- Definition 28.3 — Recursor forInductive Types
- Definition 28.4 — NegationInductive Types
- Definition 28.7 — Rules forInductive Types
- Definition 28.8 — Recursor forInductive Types
- Definition 28.12 — The partial set interpretationInductive Types
- Definition 28.17 — Rules for coproductsInductive Types
- Definition 28.18 — Case analysisInductive Types
- Definition 28.21 — Rules forInductive Types
- Definition 28.22 — Recursor forInductive Types
- Definition 28.28 — Rules for W-typesInductive Types
- Definition 28.30 — Recursor for WInductive Types
- Definition 73.39 — Set interpretation of coproducts, naturals, and W-typesInductive Types
- Definition 28.34 — A polynomial inductive signatureInductive Types
- Definition 73.47 — Dybjer's unindexed constructor schemaInductive Types
- Definition 73.49 — Strictly positive operators in the source calculusInductive Types
- Definition 29.1 — The universe hierarchy, `a la RussellUniverses and Universe Levels
- Definition 29.10 — LiftingUniverses and Universe Levels
- Definition 75.1 — The strict Tarski hierarchyTarski Universes and Decoding
- Definition 75.4 — Erasure and decorationTarski Universes and Decoding
- Definition 75.5 — Aligned conclusionsTarski Universes and Decoding
- Definition 76.1 — Hurkens's U^- interfaceUniverse Paradoxes and Hurkens's Construction
- Definition 76.2 — The Hurkens spineUniverse Paradoxes and Hurkens's Construction
- Definition 30.1 — Identity typesIdentity Types
- Definition 30.24 — Singleton typeIdentity Types
- Definition 30.28 — UIP and KIdentity Types
- Definition 30.35 — Function extensionalityIdentity Types
- Definition 78.1 — VectorsIndexed Inductive Families and Dependent Pattern Matching
- Definition 78.3 — Inductive finite indicesIndexed Inductive Families and Dependent Pattern Matching
- Definition 78.8 — Homogeneous telescopic equalityIndexed Inductive Families and Dependent Pattern Matching
- Definition 78.9 — Restricted unificationIndexed Inductive Families and Dependent Pattern Matching
- Definition 78.10 — Basic analysis and recursive hypothesesIndexed Inductive Families and Dependent Pattern Matching
- Definition 78.11 — No confusion for an indexed familyIndexed Inductive Families and Dependent Pattern Matching
- Definition 78.13 — Below complementsIndexed Inductive Families and Dependent Pattern Matching
- Definition 78.15 — Valid case treeIndexed Inductive Families and Dependent Pattern Matching
- Definition 78.18 — Root contraction of a case treeIndexed Inductive Families and Dependent Pattern Matching
- Definition 79.1 — True-record rulesDependent Records and Primitive Projections
- Definition 80.1 — Regular description codesUniverses of Datatype Descriptions and Generic Programs
- Definition 80.2 — Interpretation of descriptionsUniverses of Datatype Descriptions and Generic Programs
- Definition 80.3 — Fixed points of descriptionsUniverses of Datatype Descriptions and Generic Programs
- Definition 80.4 — Description inductionUniverses of Datatype Descriptions and Generic Programs
- Definition 80.8 — Generic foldUniverses of Datatype Descriptions and Generic Programs
- Definition 80.14 — Applicative traversal interfaceUniverses of Datatype Descriptions and Generic Programs
- Definition 80.15 — Description traversalUniverses of Datatype Descriptions and Generic Programs
- Definition 80.16 — Composite applicativeUniverses of Datatype Descriptions and Generic Programs
- Definition 80.18 — Identity applicativeUniverses of Datatype Descriptions and Generic Programs
- Definition 80.21 — Regular equality codesUniverses of Datatype Descriptions and Generic Programs
- Definition 80.26 — Binding descriptions and free syntaxUniverses of Datatype Descriptions and Generic Programs
- Definition 81.1 — Container and extensionContainers, Polynomial Functors, and Ornaments
- Definition 81.2 — Action on contentsContainers, Polynomial Functors, and Ornaments
- Definition 81.4 — Container morphismContainers, Polynomial Functors, and Ornaments
- Definition 81.5 — Identity and compositionContainers, Polynomial Functors, and Ornaments
- Definition 81.6 — Container sum and productContainers, Polynomial Functors, and Ornaments
- Definition 81.7 — Composition of containersContainers, Polynomial Functors, and Ornaments
- Definition 81.8 — Initial algebra and final coalgebraContainers, Polynomial Functors, and Ornaments
- Definition 81.11 — Indexed container and extensionContainers, Polynomial Functors, and Ornaments
- Definition 81.13 — Derivative of regular polynomial codesContainers, Polynomial Functors, and Ornaments
- Definition 81.16 — Ornament and forgetful mapContainers, Polynomial Functors, and Ornaments
- Definition 81.17 — Algebraic ornamentContainers, Polynomial Functors, and Ornaments
- Definition 82.1 — Structural-call invariantWell-Founded Recursion
- Definition 82.2 — Accessibility and well-foundednessWell-Founded Recursion
- Definition 82.4 — Accessibility eliminationWell-Founded Recursion
- Definition 82.6 — Proof-indexed well-founded recursionWell-Founded Recursion
- Definition 82.10 — Weak natural-number orderWell-Founded Recursion
- Definition 82.13 — Relation induced by a measureWell-Founded Recursion
- Definition 82.15 — Lexicographic relationWell-Founded Recursion
- Definition 82.19 — Euclidean stepWell-Founded Recursion
- Definition 82.23 — Division domainWell-Founded Recursion
- Definition 82.24 — Structural quotient on a domain proofWell-Founded Recursion
- Definition 83.1 — Size-change labelSize-Change Termination
- Definition 83.2 — Size-change matrixSize-Change Termination
- Definition 83.3 — Label product and joinSize-Change Termination
- Definition 83.4 — Matrix compositionSize-Change Termination
- Definition 83.6 — Multipath and threadSize-Change Termination
- Definition 83.7 — Safe call graphSize-Change Termination
- Definition 83.9 — Composition closure and idempotent testSize-Change Termination
- Definition 84.1 — Mendler algebraMendler Recursion, Nested Datatypes, and Mixed Variance
- Definition 84.2 — Mendler iterationMendler Recursion, Nested Datatypes, and Mixed Variance
- Definition 84.6 — Generalized fold for nested termsMendler Recursion, Nested Datatypes, and Mixed Variance
- Definition 84.8 — Lifted substitutionMendler Recursion, Nested Datatypes, and Mixed Variance
- Definition 84.9 — Nested substitutionMendler Recursion, Nested Datatypes, and Mixed Variance
- Definition 84.12 — Dependent Mendler algebraMendler Recursion, Nested Datatypes, and Mixed Variance
- Definition 84.15 — Constraint property PMendler Recursion, Nested Datatypes, and Mixed Variance
- Definition 85.1 — The guarded stream fragmentCoinduction, Copatterns, and Bisimulation
- Definition 85.2 — Finite stream observationsCoinduction, Copatterns, and Bisimulation
- Definition 85.9 — Guarded stream copattern definitionCoinduction, Copatterns, and Bisimulation
- Definition 85.10 — Observational stream equalityCoinduction, Copatterns, and Bisimulation
- Definition 85.12 — Stream bisimulationCoinduction, Copatterns, and Bisimulation
- Definition 85.18 — The T_ co record schemaCoinduction, Copatterns, and Bisimulation
- Definition 85.21 — Sized approximant formation and observationsCoinduction, Copatterns, and Bisimulation
- Definition 85.22 — Sized approximant builderCoinduction, Copatterns, and Bisimulation
- Definition 86.1 — Guarded interaction treesRecursive Effects and Interaction Trees
- Definition 86.2 — The successor serverRecursive Effects and Interaction Trees
- Definition 86.3 — Guarded bindRecursive Effects and Interaction Trees
- Definition 86.4 — Strong and weak tree bisimulationRecursive Effects and Interaction Trees
- Definition 86.7 — Handlers and interpretationRecursive Effects and Interaction Trees
- Definition 86.9 — Tagged sums of signaturesRecursive Effects and Interaction Trees
- Definition 86.10 — Visible-prefix observerRecursive Effects and Interaction Trees
- Definition 87.1 — Sequentially consistent tracesCompositional Linearizability and Modular Concurrent Objects
- Definition 87.2 — The frozen LTS specificationCompositional Linearizability and Modular Concurrent Objects
- Definition 87.3 — The artifact-local program and module interfaceCompositional Linearizability and Modular Concurrent Objects
- Definition 87.4 — Vertical and horizontal compositionCompositional Linearizability and Modular Concurrent Objects
- Definition 87.6 — Refinement and identity saturationCompositional Linearizability and Modular Concurrent Objects
- Definition 88.1 — Thread and interaction statesPossibility Reasoning and Linearizability Hoare Logic
- Definition 88.2 — Possibilities and possibility setsPossibility Reasoning and Linearizability Hoare Logic
- Definition 88.3 — Lifted possibility updatePossibility Reasoning and Linearizability Hoare Logic
- Definition 88.5 — Assertions, relations, and stabilityPossibility Reasoning and Linearizability Hoare Logic
- Definition 88.6 — Commit, silent, and return obligationsPossibility Reasoning and Linearizability Hoare Logic
- Definition 88.8 — Verified implementation familiesPossibility Reasoning and Linearizability Hoare Logic
- Definition 89.3 — Raw PCUIC termsThe Calculus of Inductive Constructions
- Definition 89.4 — Contexts and global environmentsThe Calculus of Inductive Constructions
- Definition 89.5 — Frozen well-formedness and typingThe Calculus of Inductive Constructions
- Definition 89.7 — Universe expressions and consistencyThe Calculus of Inductive Constructions
- Definition 89.8 — Cumulative conversionThe Calculus of Inductive Constructions
- Definition 89.10 — Parameters, indices, and constructor uniformityThe Calculus of Inductive Constructions
- Definition 89.11 — Cases and generated induction schemesThe Calculus of Inductive Constructions
- Definition 89.13 — Historical recursive guardsThe Calculus of Inductive Constructions
- Definition 35.1 — Extensional equality typesExtensional Type Theory
- Definition 48.30 — The set modelExtensional Type Theory
- Definition 35.13 — PropositionExtensional Type Theory
- Definition 35.18 — Propositional truncationExtensional Type Theory
- Definition 35.22 — Existence and disjunctionExtensional Type Theory
- Definition 35.24 — Small propositionsExtensional Type Theory
- Definition 35.26 — The three theoriesExtensional Type Theory
- Definition 35.27 — StrippingExtensional Type Theory
- Definition 35.31 — Paths between substitutionsExtensional Type Theory
- Definition 35.33 — Canonical comparison dataExtensional Type Theory
- Definition 35.35 — The quotient dataExtensional Type Theory
- Definition 90.47 — The modern model-theoretic endpointExtensional Type Theory
- Definition 35.43 — The SK word problemExtensional Type Theory
- Definition 35.45 — The SK context and its encodingExtensional Type Theory
- Definition 90.58 — Three decision problemsExtensional Type Theory
- Definition 91.3 — Partial equivalence relationNuprl-Style Computational Type Theory and Realizability
- Definition 91.5 — Functional PER familyNuprl-Style Computational Type Theory and Realizability
- Definition 91.6 — PER clauses for the frozen formersNuprl-Style Computational Type Theory and Realizability
- Definition 91.7 — Allen closure and universesNuprl-Style Computational Type Theory and Realizability
- Definition 91.9 — Component conversion of canonical programsNuprl-Style Computational Type Theory and Realizability
- Definition 91.14 — Closed computational judgmentsNuprl-Style Computational Type Theory and Realizability
- Definition 91.16 — False, nonnegativity, and naturalsNuprl-Style Computational Type Theory and Realizability
- Definition 91.19 — Functional contexts and equal substitutionsNuprl-Style Computational Type Theory and Realizability
- Definition 91.21 — Open computational equalityNuprl-Style Computational Type Theory and Realizability
- Definition 91.24 — The local list meaningNuprl-Style Computational Type Theory and Realizability
- Definition 91.29 — A same-subject successor specificationNuprl-Style Computational Type Theory and Realizability
- Definition 91.34 — Quotient component conversionNuprl-Style Computational Type Theory and Realizability
- Definition 91.36 — Admissible quotient relationNuprl-Style Computational Type Theory and Realizability
- Definition 92.2 — Arithmetic and small propositionsLogic-Enriched Type Theory and Predicative Mathematics
- Definition 92.3 — Small comprehensionLogic-Enriched Type Theory and Predicative Mathematics
- Definition 92.4 — Predicative recursion and inductionLogic-Enriched Type Theory and Predicative Mathematics
- Definition 93.2 — Erased dependent intersectionDependent Intersections and Same-Subject Refinement
- Definition 94.2 — Subject-dependent selfSubject-Dependent Self Types
- Definition 94.3 — Positive recursive closureSubject-Dependent Self Types
- Definition 95.2 — Very-dependent function PERVery Dependent Functions
- Definition 95.3 — Very-dependent function rulesVery Dependent Functions
- Definition 96.2 — Core type formationCDLE and Cedille: Lambda-Encoded Induction, Recursion, and Zero-Cost Reuse
- Definition 96.3 — Equality and direct computationCDLE and Cedille: Lambda-Encoded Induction, Recursion, and Zero-Cost Reuse
- Definition 97.1 — Raw terms and signaturesThe lambda-Pi-Calculus Modulo Rewriting
- Definition 97.2 — Algebraic rule cardThe lambda-Pi-Calculus Modulo Rewriting
- Definition 97.7 — Saillard's modulo-beta stepThe lambda-Pi-Calculus Modulo Rewriting
- Definition 98.1 — Types, indices, and contextsLinear Dependent Type Theory
- Definition 98.2 — ShapeLinear Dependent Type Theory
- Definition 98.3 — Kinding and context formationLinear Dependent Type Theory
- Definition 98.4 — Typing rule cardLinear Dependent Type Theory
- Definition 98.7 — Call-by-value evaluationLinear Dependent Type Theory
- Definition 98.10 — Exact imported state–parameter signatureLinear Dependent Type Theory
- Definition 99.1 — Usage semiringQuantitative Dependent Type Theory
- Definition 99.2 — JudgmentsQuantitative Dependent Type Theory
- Definition 99.4 — Dependent function rulesQuantitative Dependent Type Theory
- Definition 99.5 — Quantitative dependent tensorQuantitative Dependent Type Theory
- Definition 100.1 — Grade semiringGraded Modal Dependent Type Theory
- Definition 100.2 — Graded typing judgmentGraded Modal Dependent Type Theory
- Definition 100.3 — Core syntaxGraded Modal Dependent Type Theory
- Definition 100.4 — Function rule cardGraded Modal Dependent Type Theory
- Definition 100.5 — Dependent tensorsGraded Modal Dependent Type Theory
- Definition 100.6 — Graded modality rulesGraded Modal Dependent Type Theory
- Definition 100.7 — Discard, choose, and scaleGraded Modal Dependent Type Theory
- Definition 100.11 — The fragment GrTT^0,1Graded Modal Dependent Type Theory
- Definition 100.12 — Base terms, key redex, and saturationGraded Modal Dependent Type Theory
- Definition 101.1 — Graded-erasure signatureGraded Erasure and Extraction
- Definition 101.2 — Graded typing cardGraded Erasure and Extraction
- Definition 101.3 — Graded equality cardGraded Erasure and Extraction
- Definition 101.4 — Graded usage cardGraded Erasure and Extraction
- Definition 101.5 — Paper weak-head dynamicsGraded Erasure and Extraction
- Definition 101.8 — ExtractionGraded Erasure and Extraction
- Definition 101.9 — Non-strict target reductionGraded Erasure and Extraction
- Definition 101.12 — Resource machineGraded Erasure and Extraction
- Definition 102.1 — Dependent-session signatureDependent Session Types and Protocol-Indexed Programming
- Definition 102.2 — Structural congruence and reductionDependent Session Types and Protocol-Indexed Programming
- Definition 102.3 — Dependent quantifier rulesDependent Session Types and Protocol-Indexed Programming
- Definition 102.4 — Quantifier dualityDependent Session Types and Protocol-Indexed Programming
- Definition 102.10 — Static protocol termsDependent Session Types and Protocol-Indexed Programming
- Definition 103.1 — Fire signatureDependent Effects and Call-by-Push-Value
- Definition 103.2 — The three verticesDependent Effects and Call-by-Push-Value
- Definition 103.4 — The dCBPV rule deltaDependent Effects and Call-by-Push-Value
- Definition 103.5 — Dependent Kleisli extensionDependent Effects and Call-by-Push-Value
- Definition 103.6 — Thunkability and linearityDependent Effects and Call-by-Push-Value
- Definition 103.8 — Stacks and configurationsDependent Effects and Call-by-Push-Value
- Definition 104.1 — Weakest-precondition typesWeakest Preconditions and Dijkstra Monads
- Definition 104.2 — State and exception operationsWeakest Preconditions and Dijkstra Monads
- Definition 104.3 — The selective CPS translationWeakest Preconditions and Dijkstra Monads
- Definition 104.5 — Dijkstra computation typeWeakest Preconditions and Dijkstra Monads
- Definition 104.6 — ReificationWeakest Preconditions and Dijkstra Monads
- Definition 105.1 — Partial elementsPartiality and General Recursion in Dependent Type Theory
- Definition 105.2 — Weak equalityPartiality and General Recursion in Dependent Type Theory
- Definition 105.4 — Partial bindPartiality and General Recursion in Dependent Type Theory
- Definition 105.6 — Lifted setoids and Kleisli arrowsPartiality and General Recursion in Dependent Type Theory
- Definition 105.11 — Racing two partial elements, and a sequencePartiality and General Recursion in Dependent Type Theory
- Definition 106.1 — The system λ P_≤Dependent Subtyping, Refinement, and Graduality
- Definition 106.4 — Dependent difference refinementsDependent Subtyping, Refinement, and Graduality
- Definition 106.5 — Principal synthesis and checkingDependent Subtyping, Refinement, and Graduality
- Definition 106.11 — GCIC cast interfaceDependent Subtyping, Refinement, and Graduality
- Definition 106.12 — Context-wise reduction retractionDependent Subtyping, Refinement, and Graduality
- Definition 106.16 — Trust ledgerDependent Subtyping, Refinement, and Graduality
- Definition 107.1 — Syntax and the receiver binderDependent Object Types: Type Members, Bad Bounds, and Recursive Self
- Definition 107.2 — Typing and subtyping deltaDependent Object Types: Type Members, Bad Bounds, and Recursive Self
- Definition 107.4 — Inert type and inert contextDependent Object Types: Type Members, Bad Bounds, and Recursive Self
- Definition 107.5 — Precise and tight typingDependent Object Types: Type Members, Bad Bounds, and Recursive Self
- Definition 108.1 — Stable pathFully Path-Dependent Types: Stable Paths, Singletons, and Modules
- Definition 108.2 — Singleton path typeFully Path-Dependent Types: Stable Paths, Singletons, and Modules
- Definition 108.3 — One-occurrence path replacementFully Path-Dependent Types: Stable Paths, Singletons, and Modules
- Definition 108.7 — Path-indexed definition typingFully Path-Dependent Types: Stable Paths, Singletons, and Modules
- Definition 109.1 — Regular sequent judgmentsClassical Dependent Type Theory and Control
- Definition 109.3 — Negative-elimination-free proofClassical Dependent Type Theory and Control
- Definition 109.4 — Distinguished dependent continuationClassical Dependent Type Theory and Control
- Definition 109.7 — Type translationClassical Dependent Type Theory and Control
- Definition 109.8 — Proof translation and positive translationClassical Dependent Type Theory and Control
- Definition 48.2 — PresyntaxTrusted Kernels and Bidirectional Checking
- Definition 48.3 — Elaboration judgmentsTrusted Kernels and Bidirectional Checking
- Definition 48.8 — Normalization structureTrusted Kernels and Bidirectional Checking
- Definition 48.10 — Injective and invertible Π -typesTrusted Kernels and Bidirectional Checking
- Definition 48.11 — ConsistencyTrusted Kernels and Bidirectional Checking
- Definition 48.12 — CanonicityTrusted Kernels and Bidirectional Checking
- Definition 48.16 — Bidirectional elaborationTrusted Kernels and Bidirectional Checking
- Definition 110.22 — Independent annotation recheckTrusted Kernels and Bidirectional Checking
- Definition 48.22 — Defined elaboration contextsTrusted Kernels and Bidirectional Checking
- Definition 48.24 — Elaboration of declaration listsTrusted Kernels and Bidirectional Checking
- Definition 49.1 — Canonical formsCanonicity, Normalization, and Decidable Conversion
- Definition 49.9 — Computability assignmentCanonicity, Normalization, and Decidable Conversion
- Definition 111.18 — Level expressions in normal formCanonicity, Normalization, and Decidable Conversion
- Definition 111.20 — Root contractionCanonicity, Normalization, and Decidable Conversion
- Definition 111.22 — Reduction and weak-head reductionCanonicity, Normalization, and Decidable Conversion
- Definition 49.14 — Neutral and normal formsCanonicity, Normalization, and Decidable Conversion
- Definition 49.16 — Normalization structureCanonicity, Normalization, and Decidable Conversion
- Definition 49.23 — NbE structureCanonicity, Normalization, and Decidable Conversion
- Definition 49.24 — Kripke domainCanonicity, Normalization, and Decidable Conversion
- Definition 49.25 — Reflection, reification, evaluationCanonicity, Normalization, and Decidable Conversion
- Definition 49.30 — Kripke logical relationCanonicity, Normalization, and Decidable Conversion
- Definition 49.36 — Untyped value domainCanonicity, Normalization, and Decidable Conversion
- Definition 111.44 — Semantic operationsCanonicity, Normalization, and Decidable Conversion
- Definition 111.45 — EvaluationCanonicity, Normalization, and Decidable Conversion
- Definition 49.37 — Type-directed readbackCanonicity, Normalization, and Decidable Conversion
- Definition 111.47 — Telescope-indexed semantic substitutionsCanonicity, Normalization, and Decidable Conversion
- Definition 111.52 — World-indexed related neutral valuesCanonicity, Normalization, and Decidable Conversion
- Definition 111.57 — Natural dependent-family evidenceCanonicity, Normalization, and Decidable Conversion
- Definition 111.58 — Semantic codesCanonicity, Normalization, and Decidable Conversion
- Definition 111.59 — Semantic typesCanonicity, Normalization, and Decidable Conversion
- Definition 111.65 — The ranked Kripke relation between syntax and valuesCanonicity, Normalization, and Decidable Conversion
- Definition 111.68 — Realizing substitutionsCanonicity, Normalization, and Decidable Conversion
- Definition 111.71 — Related environments and valid pairsCanonicity, Normalization, and Decidable Conversion
- Definition 112.2 — The surface fragment T_ elabElaboration and Unification
- Definition 112.3 — Contextual metavariablesElaboration and Unification
- Definition 112.4 — Typed meta-substitution and problem-relative generalityElaboration and Unification
- Definition 112.5 — Heterogeneous constraints and solutionsElaboration and Unification
- Definition 112.6 — Generation judgmentsElaboration and Unification
- Definition 112.9 — Canonical level expressionsElaboration and Unification
- Definition 112.11 — Formation-guard compilationElaboration and Unification
- Definition 112.12 — Stratified level problemsElaboration and Unification
- Definition 112.14 — Rigid and flexible weak headsElaboration and Unification
- Definition 112.15 — Rigid simplificationElaboration and Unification
- Definition 112.17 — Direct contextual-pattern fragmentElaboration and Unification
- Definition 112.18 — Flex–rigid assignmentElaboration and Unification
- Definition 112.20 — Flex–flex intersection and insertionElaboration and Unification
- Definition 112.25 — Successful elaborationElaboration and Unification
- Definition 112.27 — The independent Timpl certificate recheckerElaboration and Unification
- Definition 112.30 — Ground-determination certificateElaboration and Unification
- Definition 112.31 — Policy-aligned generation runsElaboration and Unification
- Definition 112.34 — Reed's source language and statesElaboration and Unification
- Definition 112.35 — Dynamic-pattern transitionsElaboration and Unification
- Definition 112.39 — Delayed implicit-abstraction insertionElaboration and Unification
- Definition 113.1 — Shared term DAG and its tree solutionsEfficient First-Order Unification
- Definition 113.2 — Homogeneous acyclic congruenceEfficient First-Order Unification
- Definition 113.4 — Root-class graph unificationEfficient First-Order Unification
- Definition 113.7 — Paterson–Wegman scheduling interfaceEfficient First-Order Unification
- Definition 114.1 — Goals and proof statesProof-Producing Tactics and the Kernel Boundary
- Definition 114.2 — Primitive proof-producing tacticsProof-Producing Tactics and the Kernel Boundary
- Definition 114.4 — Tactic evaluationProof-Producing Tactics and the Kernel Boundary
- Definition 114.6 — Closing a proof stateProof-Producing Tactics and the Kernel Boundary
- Definition 114.8 — Case-split certificateProof-Producing Tactics and the Kernel Boundary
- Definition 114.9 — Replay certificateProof-Producing Tactics and the Kernel Boundary
- Definition 115.1 — Certified rewrite databaseRewriting, Simplification, and Reflection
- Definition 115.2 — Contextual congruence certificatesRewriting, Simplification, and Reflection
- Definition 115.3 — Simplification algorithmRewriting, Simplification, and Reflection
- Definition 115.5 — Dependent respectful function relationRewriting, Simplification, and Reflection
- Definition 115.6 — Contextual rewriting judgmentRewriting, Simplification, and Reflection
- Definition 115.8 — Reflected commutative-monoid expressionsRewriting, Simplification, and Reflection
- Definition 116.1 — Scoped identifiers and occurrence identityTyped Metaprogramming and Hygienic Elaboration
- Definition 116.2 — Raw and scoped syntaxTyped Metaprogramming and Hygienic Elaboration
- Definition 116.3 — Provenance on scoped syntaxTyped Metaprogramming and Hygienic Elaboration
- Definition 116.4 — Hygienic expansion with provenanceTyped Metaprogramming and Hygienic Elaboration
- Definition 116.6 — Staged typingTyped Metaprogramming and Hygienic Elaboration
- Definition 116.7 — Source typingTyped Metaprogramming and Hygienic Elaboration
- Definition 116.9 — Source–scoped compatibilityTyped Metaprogramming and Hygienic Elaboration
- Definition 116.11 — Checked macro expansionTyped Metaprogramming and Hygienic Elaboration
- Definition 116.12 — Checked command expansionTyped Metaprogramming and Hygienic Elaboration
- Definition 117.2 — First-class level rulesFirst-Class Universe Levels and Level Polymorphism
- Definition 117.3 — Lift rulesFirst-Class Universe Levels and Level Polymorphism
- Definition 117.5 — Level abstractionFirst-Class Universe Levels and Level Polymorphism
- Definition 117.7 — Level polynomial normal formFirst-Class Universe Levels and Level Polymorphism
- Definition 118.2 — Sort abstraction and applicationSort Polymorphism and Stratified Type Theory
- Definition 118.3 — Elimination constraintsSort Polymorphism and Stratified Type Theory
- Definition 118.5 — Finite sort constraintsSort Polymorphism and Stratified Type Theory
- Definition 118.7 — MonomorphizationSort Polymorphism and Stratified Type Theory
- Definition 118.12 — Valid bounded-sort constraintsSort Polymorphism and Stratified Type Theory
- Definition 119.2 — Context-indexed coercion signature and pathsCoercive Subtyping and Coherent Cast Insertion
- Definition 119.4 — Subsumptive source judgmentCoercive Subtyping and Coherent Cast Insertion
- Definition 119.6 — Coercion-inserting elaborationCoercive Subtyping and Coherent Cast Insertion
- Definition 120.2 — Positive descriptionsDefinitional Functoriality and Generic Type-Former Action
- Definition 120.3 — Generated actionDefinitional Functoriality and Generic Type-Former Action
- Definition 120.5 — Functoriality rule deltaDefinitional Functoriality and Generic Type-Former Action
- Definition 120.7 — Indexed descriptionsDefinitional Functoriality and Generic Type-Former Action
- Definition 120.9 — Map compactionDefinitional Functoriality and Generic Type-Former Action
- Definition 120.10 — Typed evaluation contextsDefinitional Functoriality and Generic Type-Former Action
- Definition 121.1 — The Timpl-clauses system cardCompiling Dependent Pattern Matching
- Definition 121.3 — Nondependent clause matricesCompiling Dependent Pattern Matching
- Definition 121.5 — Readiness by relevanceCompiling Dependent Pattern Matching
- Definition 121.6 — Pattern matching and the source stepCompiling Dependent Pattern Matching
- Definition 121.8 — Raw rows and their written mapsCompiling Dependent Pattern Matching
- Definition 121.9 — Typed case treesCompiling Dependent Pattern Matching
- Definition 121.10 — Valid Timpl-clauses treeCompiling Dependent Pattern Matching
- Definition 121.11 — Restricted-unifier scheduleCompiling Dependent Pattern Matching
- Definition 121.12 — The leftmost compilerCompiling Dependent Pattern Matching
- Definition 122.1 — The Timpl-data system cardDatatype Declaration Blocks and Strict Positivity
- Definition 122.2 — The Tfam-block rule schemaDatatype Declaration Blocks and Strict Positivity
- Definition 122.3 — Dependency orderDatatype Declaration Blocks and Strict Positivity
- Definition 122.4 — Occurrence checkDatatype Declaration Blocks and Strict Positivity
- Definition 122.5 — Datatype-block rejection diagnosticDatatype Declaration Blocks and Strict Positivity
- Definition 122.8 — Hypothesis typeDatatype Declaration Blocks and Strict Positivity
- Definition 122.12 — Constructor-by-constructor block translationDatatype Declaration Blocks and Strict Positivity
- Definition 122.13 — Universe outputDatatype Declaration Blocks and Strict Positivity
- Definition 123.1 — The Timpl-rec system cardRecursive Function Groups and Termination
- Definition 123.2 — Function call graphRecursive Function Groups and Termination
- Definition 123.3 — Structural descent judgmentRecursive Function Groups and Termination
- Definition 123.4 — Lexicographic call certificateRecursive Function Groups and Termination
- Definition 123.5 — Recursive-group rejection diagnosticRecursive Function Groups and Termination
- Definition 123.7 — Mutual-block carrier and direct-child relationRecursive Function Groups and Termination
- Definition 123.10 — The certified tagged call relationRecursive Function Groups and Termination
- Definition 123.13 — Body translationRecursive Function Groups and Termination
- Definition 123.15 — Closed source and recursive-core evaluationRecursive Function Groups and Termination
- Definition 124.1 — The Timpl-co system cardCorecursive Definitions, Copatterns, and Productivity
- Definition 124.2 — Source stream declaration dynamicsCorecursive Definitions, Copatterns, and Productivity
- Definition 124.5 — Finite observationsCorecursive Definitions, Copatterns, and Productivity
- Definition 124.6 — Guard-weighted call graphCorecursive Definitions, Copatterns, and Productivity
- Definition 124.11 — CoiteratorCorecursive Definitions, Copatterns, and Productivity
- Definition 125.1 — The dependent-copattern elaboration cardElaborating Dependent Copattern Definitions
- Definition 125.2 — Tcop-clause typing and source observationElaborating Dependent Copattern Definitions
- Definition 125.3 — Tcop-tree syntax and executionElaborating Dependent Copattern Definitions
- Definition 125.4 — Typed copattern frontierElaborating Dependent Copattern Definitions
- Definition 125.5 — Copattern splittingElaborating Dependent Copattern Definitions
- Definition 125.9 — The Tcop-core record corecursorElaborating Dependent Copattern Definitions
- Definition 125.10 — Generated copattern state blockElaborating Dependent Copattern Definitions
- Definition 125.12 — Tree-to-core translationElaborating Dependent Copattern Definitions
- Definition 125.15 — Compiled application preparationElaborating Dependent Copattern Definitions
- Definition 125.17 — Tcop-core observationElaborating Dependent Copattern Definitions
- Definition 126.1 — The Timpl-erasure system cardErasure and Execution of Dependent Definitions
- Definition 126.3 — Runtime relevanceErasure and Execution of Dependent Definitions
- Definition 126.5 — Source call-by-value evaluationErasure and Execution of Dependent Definitions
- Definition 126.9 — Relevance annotation of an accepted declarationErasure and Execution of Dependent Definitions
- Definition 126.10 — ErasureErasure and Execution of Dependent Definitions
- Definition 126.12 — Value representationErasure and Execution of Dependent Definitions
- Definition 126.15 — The Timpl-co-erasure cardErasure and Execution of Dependent Definitions
- Definition 126.21 — The System Fi-to-F_ω cardErasure and Execution of Dependent Definitions
- Definition 127.1 — Scheme0 source cardPartial Evaluation, Binding-Time Analysis, and the Futamura Projections
- Definition 127.2 — The pe_ on numeric projectionPartial Evaluation, Binding-Time Analysis, and the Futamura Projections
- Definition 127.5 — Fuelled specializationPartial Evaluation, Binding-Time Analysis, and the Futamura Projections
- Definition 127.6 — Completed-table invariantPartial Evaluation, Binding-Time Analysis, and the Futamura Projections
- Definition 127.12 — Completed offline specialization graphPartial Evaluation, Binding-Time Analysis, and the Futamura Projections
- Definition 128.1 — SC-CBV state spaceSupercompilation, Driving, and Generalization
- Definition 128.6 — SC-CBV improvementSupercompilation, Driving, and Generalization
- Definition 128.11 — Admissible driver stateSupercompilation, Driving, and Generalization
- Definition 131.1 — Symbol classes and raw syntaxExplicit Equality Evidence and System FC
- Definition 131.2 — Kind well-formednessExplicit Equality Evidence and System FC
- Definition 131.3 — Type kindingExplicit Equality Evidence and System FC
- Definition 131.6 — Coercion kindingExplicit Equality Evidence and System FC
- Definition 131.7 — Term typing and patternsExplicit Equality Evidence and System FC
- Definition 131.8 — Declarations and programsExplicit Equality Evidence and System FC
- Definition 131.21 — Values, cvalues, contextsExplicit Equality Evidence and System FC
- Definition 131.22 — ReductionExplicit Equality Evidence and System FC
- Definition 131.28 — Value typeExplicit Equality Evidence and System FC
- Definition 131.29 — ConsistencyExplicit Equality Evidence and System FC
- Definition 131.34 — ErasureExplicit Equality Evidence and System FC
- Definition 131.37 — ElaborationExplicit Equality Evidence and System FC
- Definition 132.1 — Syntax of DSystems D and DC: A Dependent Haskell Core Specification
- Definition 132.2 — ReductionSystems D and DC: A Dependent Haskell Core Specification
- Definition 132.3 — TypingSystems D and DC: A Dependent Haskell Core Specification
- Definition 132.5 — Definitional equalitySystems D and DC: A Dependent Haskell Core Specification
- Definition 132.12 — Consistent typesSystems D and DC: A Dependent Haskell Core Specification
- Definition 132.13 — JoinabilitySystems D and DC: A Dependent Haskell Core Specification
- Definition 132.20 — Syntax of DCSystems D and DC: A Dependent Haskell Core Specification
- Definition 132.21 — Typing for DCSystems D and DC: A Dependent Haskell Core Specification
- Definition 132.22 — Coercion checking, excerptSystems D and DC: A Dependent Haskell Core Specification
- Definition 132.26 — Annotation erasureSystems D and DC: A Dependent Haskell Core Specification
- Definition 133.1 — λ ^FTyped Intermediate Languages and Certified Closure Conversion
- Definition 133.2 — λ ^KTyped Intermediate Languages and Certified Closure Conversion
- Definition 133.3 — CPS translationTyped Intermediate Languages and Certified Closure Conversion
- Definition 133.5 — λ ^CTyped Intermediate Languages and Certified Closure Conversion
- Definition 133.9 — λ ^ATyped Intermediate Languages and Certified Closure Conversion
- Definition 133.12 — TALTyped Intermediate Languages and Certified Closure Conversion
- Definition 133.18 — The exported interfacesTyped Intermediate Languages and Certified Closure Conversion
- Definition 134.1 — Intrinsically typed source syntaxA Certified Type-Preserving Compiler to Assembly
- Definition 134.3 — Denotation of the source languageA Certified Type-Preserving Compiler to Assembly
- Definition 134.4 — LinearA Certified Type-Preserving Compiler to Assembly
- Definition 134.5 — SplicingA Certified Type-Preserving Compiler to Assembly
- Definition 134.10 — The lower languagesA Certified Type-Preserving Compiler to Assembly
- Definition 134.11 — TracesA Certified Type-Preserving Compiler to Assembly
- Definition 134.12 — Heaps, tags and failureA Certified Type-Preserving Compiler to Assembly
- Definition 134.13 — The CPS–CC relationA Certified Type-Preserving Compiler to Assembly
- Definition 134.16 — Pointer isomorphismA Certified Type-Preserving Compiler to Assembly
- Definition 134.20 — The trusted computing baseA Certified Type-Preserving Compiler to Assembly
- Definition 135.1 — The higher-order call-by-name evaluatorDefunctionalization, Refunctionalization, and Abstract Machines
- Definition 135.2 — The closure-converted evaluatorDefunctionalization, Refunctionalization, and Abstract Machines
- Definition 135.4 — The continuation-passing evaluatorDefunctionalization, Refunctionalization, and Abstract Machines
- Definition 135.6 — The defunctionalized evaluatorDefunctionalization, Refunctionalization, and Abstract Machines
- Definition 135.13 — Defunctionalized formDefunctionalization, Refunctionalization, and Abstract Machines
- Definition 136.1 — Programs, contexts, tracesSecure Compilation and Robust Property Preservation
- Definition 136.2 — Properties and behavioursSecure Compilation and Robust Property Preservation
- Definition 136.3 — Robust trace property preservationSecure Compilation and Robust Property Preservation
- Definition 136.4 — Property-free characterizationSecure Compilation and Robust Property Preservation
- Definition 136.6 — Safety and dense propertiesSecure Compilation and Robust Property Preservation
- Definition 136.7 — The two criteriaSecure Compilation and Robust Property Preservation
- Definition 136.10 — Robust hyperproperty preservationSecure Compilation and Robust Property Preservation
- Definition 136.13 — Observational equivalence preservationSecure Compilation and Robust Property Preservation
- Definition 136.17 — Context-based back-translationSecure Compilation and Robust Property Preservation
- Definition 136.18 — Trace-based back-translationSecure Compilation and Robust Property Preservation
- Definition 137.1 — CCDependent Closure Conversion for the Calculus of Constructions
- Definition 137.2 — TypingDependent Closure Conversion for the Calculus of Constructions
- Definition 137.6 — CC-CCDependent Closure Conversion for the Calculus of Constructions
- Definition 137.7 — Closure equivalenceDependent Closure Conversion for the Calculus of Constructions
- Definition 137.9 — Closure conversionDependent Closure Conversion for the Calculus of Constructions
- Definition 137.20 — Components and linkingDependent Closure Conversion for the Calculus of Constructions
- Definition 138.1 — SourceDependency-Preserving A-Normal Form
- Definition 138.2 — A-normal formDependency-Preserving A-Normal Form
- Definition 138.3 — Definitions in the contextDependency-Preserving A-Normal Form
- Definition 138.5 — Dependent if with recorded equalitiesDependency-Preserving A-Normal Form
- Definition 138.8 — Continuation typingDependency-Preserving A-Normal Form
- Definition 138.12 — ANF translationDependency-Preserving A-Normal Form
- Definition 139.1 — SyntaxTyped Functional Array Languages: Shapes, Uniqueness, and Parallel Compilation
- Definition 139.2 — Witnessed sizesTyped Functional Array Languages: Shapes, Uniqueness, and Parallel Compilation
- Definition 139.3 — TypingTyped Functional Array Languages: Shapes, Uniqueness, and Parallel Compilation
- Definition 139.4 — Dynamic semanticsTyped Functional Array Languages: Shapes, Uniqueness, and Parallel Compilation
- Definition 139.6 — Value equivalenceTyped Functional Array Languages: Shapes, Uniqueness, and Parallel Compilation
- Definition 139.11 — The logical relationTyped Functional Array Languages: Shapes, Uniqueness, and Parallel Compilation
- Definition 140.1 — Raw, scoped and well-formed syntaxVerified Metatheory and Realistic Trusted Kernels
- Definition 140.2 — UniversesVerified Metatheory and Realistic Trusted Kernels
- Definition 140.3 — Parallel reductionVerified Metatheory and Realistic Trusted Kernels
- Definition 140.9 — The oraclesVerified Metatheory and Realistic Trusted Kernels
- Definition 140.10 — NormalizationVerified Metatheory and Realistic Trusted Kernels
- Definition 140.13 — Inference as a correct-by-construction functionVerified Metatheory and Realistic Trusted Kernels
- Definition 140.17 — The target calculusVerified Metatheory and Realistic Trusted Kernels
- Definition 140.18 — The erasure functionVerified Metatheory and Realistic Trusted Kernels
- Definition 140.20 — The erasure relationVerified Metatheory and Realistic Trusted Kernels
- Definition 140.25 — What remains trustedVerified Metatheory and Realistic Trusted Kernels
- Definition 141.1 — Substitutions between contextsCategories, Functors, and Representability
- Definition 141.4 — Composition and identityCategories, Functors, and Representability
- Definition 141.8 — CategoryCategories, Functors, and Representability
- Definition 141.17 — Free category on a graphCategories, Functors, and Representability
- Definition 141.21 — IsomorphismCategories, Functors, and Representability
- Definition 141.23 — GroupoidCategories, Functors, and Representability
- Definition 141.25 — Opposite categoryCategories, Functors, and Representability
- Definition 141.26 — Terminal and initial objectsCategories, Functors, and Representability
- Definition 141.28 — Monomorphism, epimorphismCategories, Functors, and Representability
- Definition 141.30 — Global elementsCategories, Functors, and Representability
- Definition 141.32 — FunctorCategories, Functors, and Representability
- Definition 141.38 — PresheafCategories, Functors, and Representability
- Definition 141.41 — Natural transformationCategories, Functors, and Representability
- Definition 141.44 — Full, faithful, essentially surjectiveCategories, Functors, and Representability
- Definition 141.45 — Equivalence of categoriesCategories, Functors, and Representability
- Definition 141.50 — RepresentationCategories, Functors, and Representability
- Definition 141.54 — Product categoryCategories, Functors, and Representability
- Definition 141.58 — Yoneda embeddingCategories, Functors, and Representability
- Definition 141.64 — Category of elementsCategories, Functors, and Representability
- Definition 142.1 — Binary productAdjunctions, Limits, and Locally Cartesian Closure
- Definition 142.8 — PullbackAdjunctions, Limits, and Locally Cartesian Closure
- Definition 142.10 — The syntactic category of a dependent theoryAdjunctions, Limits, and Locally Cartesian Closure
- Definition 142.12 — EqualizerAdjunctions, Limits, and Locally Cartesian Closure
- Definition 142.14 — Diagram, cone, limitAdjunctions, Limits, and Locally Cartesian Closure
- Definition 142.17 — Adjunction, hom-set formAdjunctions, Limits, and Locally Cartesian Closure
- Definition 142.20 — Unit and counit formAdjunctions, Limits, and Locally Cartesian Closure
- Definition 142.26 — Cartesian closed categoryAdjunctions, Limits, and Locally Cartesian Closure
- Definition 142.29 — The category of contexts modulo conversionAdjunctions, Limits, and Locally Cartesian Closure
- Definition 142.31 — Slice categoryAdjunctions, Limits, and Locally Cartesian Closure
- Definition 142.33 — Substitution and dependent sumAdjunctions, Limits, and Locally Cartesian Closure
- Definition 142.36 — Locally cartesian closedAdjunctions, Limits, and Locally Cartesian Closure
- Definition 143.1 — Heyting algebraCategorical Logic, Hyperdoctrines, and Internal Languages
- Definition 143.7 — Beck–Chevalley conditionCategorical Logic, Hyperdoctrines, and Internal Languages
- Definition 143.8 — HyperdoctrineCategorical Logic, Hyperdoctrines, and Internal Languages
- Definition 143.14 — Equality predicateCategorical Logic, Hyperdoctrines, and Internal Languages
- Definition 143.17 — ComprehensionCategorical Logic, Hyperdoctrines, and Internal Languages
- Definition 143.20 — Signature, terms, formulas, sequentsCategorical Logic, Hyperdoctrines, and Internal Languages
- Definition 143.21 — Derivable sequentsCategorical Logic, Hyperdoctrines, and Internal Languages
- Definition 143.22 — InterpretationCategorical Logic, Hyperdoctrines, and Internal Languages
- Definition 143.29 — Internal languageCategorical Logic, Hyperdoctrines, and Internal Languages
- Definition 144.1 — Heyting pre-algebraTriposes, Toposes, and Realizability
- Definition 144.2 — TriposTriposes, Toposes, and Realizability
- Definition 144.5 — Partial applicative structureTriposes, Toposes, and Realizability
- Definition 144.10 — P-valued setTriposes, Toposes, and Realizability
- Definition 144.12 — Relations and functional relationsTriposes, Toposes, and Realizability
- Definition 144.13 — The category of P-setsTriposes, Toposes, and Realizability
- Definition 144.18 — Canonical monomorphismTriposes, Toposes, and Realizability
- Definition 144.22 — The P-set of numbersTriposes, Toposes, and Realizability
- Definition 145.1 — Terms, stacks, processesClassical Realizability, Poles, and Orthogonality
- Definition 145.2 — The Krivine machineClassical Realizability, Poles, and Orthogonality
- Definition 145.4 — Krivine numeralsClassical Realizability, Poles, and Orthogonality
- Definition 145.5 — PoleClassical Realizability, Poles, and Orthogonality
- Definition 145.6 — OrthogonalClassical Realizability, Poles, and Orthogonality
- Definition 145.9 — Formulas with parametersClassical Realizability, Poles, and Orthogonality
- Definition 145.10 — Falsity and truth valuesClassical Realizability, Poles, and Orthogonality
- Definition 145.15 — Identity-likeClassical Realizability, Poles, and Orthogonality
- Definition 145.18 — The system λ NK_2Classical Realizability, Poles, and Orthogonality
- Definition 145.19 — Valuation, closure, adequacyClassical Realizability, Poles, and Orthogonality
- Definition 54.2 — The substitution calculusAlgebraic Syntax, CwFs, and Initiality
- Definition 54.8 — LiftingAlgebraic Syntax, CwFs, and Initiality
- Definition 54.9 — Π in the substitution calculusAlgebraic Syntax, CwFs, and Initiality
- Definition 54.15 — Families of setsAlgebraic Syntax, CwFs, and Initiality
- Definition 54.16 — Category with familiesAlgebraic Syntax, CwFs, and Initiality
- Definition 54.19 — Semantic liftingAlgebraic Syntax, CwFs, and Initiality
- Definition 54.21 — Π -structureAlgebraic Syntax, CwFs, and Initiality
- Definition 54.22 — Σ -structureAlgebraic Syntax, CwFs, and Initiality
- Definition 54.23 — Id-structureAlgebraic Syntax, CwFs, and Initiality
- Definition 54.24 — Universe structureAlgebraic Syntax, CwFs, and Initiality
- Definition 116.28 — Models of the fixed signatureAlgebraic Syntax, CwFs, and Initiality
- Definition 54.26 — Strict CwF-morphismAlgebraic Syntax, CwFs, and Initiality
- Definition 54.32 — Groupoids and familiesAlgebraic Syntax, CwFs, and Initiality
- Definition 116.40 — Vertical transformations of dependent sectionsAlgebraic Syntax, CwFs, and Initiality
- Definition 54.33 — The groupoid CwFAlgebraic Syntax, CwFs, and Initiality
- Definition 147.3 — Uniform familyGeneralized Algebraic Theories
- Definition 147.4 — PresentationGeneralized Algebraic Theories
- Definition 147.15 — The frozen second-order signature languageGeneralized Algebraic Theories
- Definition 148.1 — SyntaxExplicit-Substitution Calculi
- Definition 148.2 — The rulesExplicit-Substitution Calculi
- Definition 148.11 — Syntax and equationExplicit-Substitution Calculi
- Definition 148.12 — The rulesExplicit-Substitution Calculi
- Definition 149.2 — The indexed categoryCategorical Semantics of Scoped Operations
- Definition 149.3 — Shift left and shift rightCategorical Semantics of Scoped Operations
- Definition 149.5 — Scoped algebraCategorical Semantics of Scoped Operations
- Definition 149.8 — The free scoped monadCategorical Semantics of Scoped Operations
- Definition 149.11 — BracketingCategorical Semantics of Scoped Operations
- Definition 150.2 — Indexed comonadCategorical Semantics of Coeffects
- Definition 150.6 — Indexed lax and colax monoidal structureCategorical Semantics of Coeffects
- Definition 150.8 — InterpretationCategorical Semantics of Coeffects
- Definition 151.3 — The set model SSet and CwF Models of Type Theory
- Definition 151.29 — Displayed CwFSet and CwF Models of Type Theory
- Definition 152.1 — GroupoidGroupoid and Path-Object Models of Intensional Type Theory
- Definition 152.6 — Families and dependent objectsGroupoid and Path-Object Models of Intensional Type Theory
- Definition 152.11 — The identity familyGroupoid and Path-Object Models of Intensional Type Theory
- Definition 152.21 — The groupoid universeGroupoid and Path-Object Models of Intensional Type Theory
- Definition 152.25 — Display maps and path objectsGroupoid and Path-Object Models of Intensional Type Theory
- Definition 153.1 — SetoidSetoid and PER Models of Type Theory
- Definition 153.2 — Product and exponentSetoid and PER Models of Type Theory
- Definition 153.3 — LevelsSetoid and PER Models of Type Theory
- Definition 153.6 — Proof-irrelevant familySetoid and PER Models of Type Theory
- Definition 153.8 — Global elements, sum and productSetoid and PER Models of Type Theory
- Definition 153.16 — Bracket typesSetoid and PER Models of Type Theory
- Definition 153.19 — Iterative setsSetoid and PER Models of Type Theory
- Definition 153.21 — Decoding a code to a setoidSetoid and PER Models of Type Theory
- Definition 153.27 — Applicative structure and PERsSetoid and PER Models of Type Theory
- Definition 153.28 — The category of PERsSetoid and PER Models of Type Theory
- Definition 153.30 — Families of PERs and their formersSetoid and PER Models of Type Theory
- Definition 154.1 — Types and termsRecursive Domain Semantics and Computational Adequacy
- Definition 154.2 — Values, evaluation contexts, transitionsRecursive Domain Semantics and Computational Adequacy
- Definition 154.4 — Finite effect valuesRecursive Domain Semantics and Computational Adequacy
- Definition 154.7 — Dcpos and continuityRecursive Domain Semantics and Computational Adequacy
- Definition 154.11 — Evaluation into the tree domainRecursive Domain Semantics and Computational Adequacy
- Definition 154.14 — InterpretationRecursive Domain Semantics and Computational Adequacy
- Definition 154.20 — The approximation languageRecursive Domain Semantics and Computational Adequacy
- Definition 155.2 — The universal pre-domainDependent PER-Enriched Domain Models
- Definition 155.4 — Complete, admissible, monotoneDependent PER-Enriched Domain Models
- Definition 155.7 — Assemblies and uniform familiesDependent PER-Enriched Domain Models
- Definition 155.8 — ReindexingDependent PER-Enriched Domain Models
- Definition 155.14 — The fixed-point realizerDependent PER-Enriched Domain Models
- Definition 156.3 — Comprehension categoryCoherence and Local Universes
- Definition 156.4 — Weak and strict stabilityCoherence and Local Universes
- Definition 156.6 — The comprehension category C_!Coherence and Local Universes
- Definition 156.9 — Dependent exponentials and condition (LF)Coherence and Local Universes
- Definition 157.1 — ArenaGames, Arenas, and Strategies
- Definition 157.3 — Product and arrowGames, Arenas, and Strategies
- Definition 157.4 — Justified sequences and playsGames, Arenas, and Strategies
- Definition 157.6 — StrategyGames, Arenas, and Strategies
- Definition 157.7 — Interaction and compositionGames, Arenas, and Strategies
- Definition 157.10 — CopycatGames, Arenas, and Strategies
- Definition 157.12 — InnocenceGames, Arenas, and Strategies
- Definition 157.17 — Interpretation of types and constantsGames, Arenas, and Strategies
- Definition 157.19 — RecursionGames, Arenas, and Strategies
- Definition 158.1 — Contexts and contextual approximationDefinability and Full Abstraction for PCF
- Definition 158.4 — Intrinsic preorderDefinability and Full Abstraction for PCF
- Definition 158.6 — CompactnessDefinability and Full Abstraction for PCF
- Definition 158.8 — η -long form of a typeDefinability and Full Abstraction for PCF
- Definition 159.1 — Tensor dataSymmetric Monoidal Categories and Graphical Linear Semantics
- Definition 159.5 — Monoidal categorySymmetric Monoidal Categories and Graphical Linear Semantics
- Definition 159.7 — Braiding and symmetrySymmetric Monoidal Categories and Graphical Linear Semantics
- Definition 159.10 — Typed signatureSymmetric Monoidal Categories and Graphical Linear Semantics
- Definition 159.14 — DiagramsSymmetric Monoidal Categories and Graphical Linear Semantics
- Definition 159.17 — Monoidal closedSymmetric Monoidal Categories and Graphical Linear Semantics
- Definition 159.19 — Interpretation of λ _ linSymmetric Monoidal Categories and Graphical Linear Semantics
- Definition 159.24 — Linear–nonlinear adjunctionSymmetric Monoidal Categories and Graphical Linear Semantics
- Definition 159.27 — Lax, oplax, strongSymmetric Monoidal Categories and Graphical Linear Semantics
- Definition 160.1 — The Fitch-style calculusModal and Multimodal Dependent Type Theory
- Definition 160.5 — The dependent lock calculusModal and Multimodal Dependent Type Theory
- Definition 160.6 — CwF with a dependent right adjointModal and Multimodal Dependent Type Theory
- Definition 160.10 — Mode theoryModal and Multimodal Dependent Type Theory
- Definition 160.11 — Multimodal syntaxModal and Multimodal Dependent Type Theory
- Definition 160.15 — The guarded mode theoryModal and Multimodal Dependent Type Theory
- Definition 161.1 — The Boolean–product signatureSynthetic Phase Distinctions and Synthetic Tait Computability
- Definition 161.3 — Canonicity for ΣSynthetic Phase Distinctions and Synthetic Tait Computability
- Definition 161.5 — Syntactic category, presheaves, pointsSynthetic Phase Distinctions and Synthetic Tait Computability
- Definition 161.6 — Artin gluingSynthetic Phase Distinctions and Synthetic Tait Computability
- Definition 161.8 — Phase-separated interpretationSynthetic Phase Distinctions and Synthetic Tait Computability
- Definition 161.10 — The syntactic phaseSynthetic Phase Distinctions and Synthetic Tait Computability
- Definition 161.12 — Modal typesSynthetic Phase Distinctions and Synthetic Tait Computability
- Definition 161.17 — Partial elements and extentsSynthetic Phase Distinctions and Synthetic Tait Computability
- Definition 161.19 — Isomorphs and realignmentSynthetic Phase Distinctions and Synthetic Tait Computability
- Definition 161.23 — Strict glue typeSynthetic Phase Distinctions and Synthetic Tait Computability
- Definition 162.2 — Delayed substitutionsGuarded and Clocked Dependent Type Theory
- Definition 162.3 — Equations of the guarded calculusGuarded and Clocked Dependent Type Theory
- Definition 162.5 — Guarded recursion and L"ob inductionGuarded and Clocked Dependent Type Theory
- Definition 162.7 — Guarded streamsGuarded and Clocked Dependent Type Theory
- Definition 162.9 — The category SGuarded and Clocked Dependent Type Theory
- Definition 162.10 — The later functorGuarded and Clocked Dependent Type Theory
- Definition 162.13 — Contractive morphismsGuarded and Clocked Dependent Type Theory
- Definition 162.15 — Semantics of contexts, types and termsGuarded and Clocked Dependent Type Theory
- Definition 162.19 — Finite observationsGuarded and Clocked Dependent Type Theory
- Definition 162.24 — Clock contexts and clock quantificationGuarded and Clocked Dependent Type Theory
- Definition 162.26 — Coinductive streamsGuarded and Clocked Dependent Type Theory
- Definition 163.3 — Predicates and the later operatorSynthetic Guarded Domain Theory and Step-Indexed Semantics
- Definition 163.6 — The lifting objectSynthetic Guarded Domain Theory and Step-Indexed Semantics
- Definition 163.8 — Divergence and the monad structureSynthetic Guarded Domain Theory and Step-Indexed Semantics
- Definition 163.10 — The heap objectSynthetic Guarded Domain Theory and Step-Indexed Semantics
- Definition 163.13 — The calculus Λ _ cellSynthetic Guarded Domain Theory and Step-Indexed Semantics
- Definition 163.16 — Interpretation of types and termsSynthetic Guarded Domain Theory and Step-Indexed Semantics
- Definition 163.24 — The guarded relationsSynthetic Guarded Domain Theory and Step-Indexed Semantics
- Definition 163.29 — Chain-complete posets and continuous mapsSynthetic Guarded Domain Theory and Step-Indexed Semantics
- Definition 164.1 — Relational interpretation of simple typesDependent Parametricity
- Definition 164.4 — The signature SDependent Parametricity
- Definition 164.6 — Translation of types and termsDependent Parametricity
- Definition 164.7 — Translation of the remaining formersDependent Parametricity
- Definition 164.11 — The counter interfaceDependent Parametricity
- Definition 164.16 — Identity extensionDependent Parametricity
- Definition 164.19 — The parametricity axiomDependent Parametricity
- Definition 165.1 — Sizes, measures, size contextsSized Copattern Recursion and Mixed Induction–Coinduction
- Definition 165.2 — Size comparisonSized Copattern Recursion and Mixed Induction–Coinduction
- Definition 165.3 — Consistent extensionSized Copattern Recursion and Mixed Induction–Coinduction
- Definition 165.5 — Simple kinds, kinds, variancesSized Copattern Recursion and Mixed Induction–Coinduction
- Definition 165.6 — Type constructorsSized Copattern Recursion and Mixed Induction–Coinduction
- Definition 165.7 — SubtypingSized Copattern Recursion and Mixed Induction–Coinduction
- Definition 165.9 — Sized inductive and coinductive typesSized Copattern Recursion and Mixed Induction–Coinduction
- Definition 165.11 — SyntaxSized Copattern Recursion and Mixed Induction–Coinduction
- Definition 165.12 — Matching and reductionSized Copattern Recursion and Mixed Induction–Coinduction
- Definition 165.13 — Declarations and programsSized Copattern Recursion and Mixed Induction–Coinduction
- Definition 165.14 — Clause typingSized Copattern Recursion and Mixed Induction–Coinduction
- Definition 165.15 — Measured recursionSized Copattern Recursion and Mixed Induction–Coinduction
- Definition 165.16 — The types of eq:sc-spSized Copattern Recursion and Mixed Induction–Coinduction
- Definition 165.20 — Neutral and terminally stuckSized Copattern Recursion and Mixed Induction–Coinduction
- Definition 165.21 — Reducibility candidateSized Copattern Recursion and Mixed Induction–Coinduction
- Definition 165.23 — Semantic type formersSized Copattern Recursion and Mixed Induction–Coinduction
- Definition 165.25 — Semantic sized fixed pointsSized Copattern Recursion and Mixed Induction–Coinduction
- Definition 165.28 — Semantic judgmentsSized Copattern Recursion and Mixed Induction–Coinduction
- Definition 166.3 — Sizes and their orderParametric Large Sizes and Realizability Consistency
- Definition 166.4 — Parametric quantifiersParametric Large Sizes and Realizability Consistency
- Definition 166.5 — Well-founded induction on sizesParametric Large Sizes and Realizability Consistency
- Definition 166.8 — The four commuting axiomsParametric Large Sizes and Realizability Consistency
- Definition 166.10 — Functors and size-indexed functorsParametric Large Sizes and Realizability Consistency
- Definition 166.11 — AlgebrasParametric Large Sizes and Realizability Consistency
- Definition 166.14 — Weak commutation with the existentialParametric Large Sizes and Realizability Consistency
- Definition 166.19 — Coalgebras and weak commutation with the universalParametric Large Sizes and Realizability Consistency
- Definition 166.23 — AssembliesParametric Large Sizes and Realizability Consistency
- Definition 166.24 — Modest sets and partial equivalence relationsParametric Large Sizes and Realizability Consistency
- Definition 166.26 — The modelParametric Large Sizes and Realizability Consistency
- Definition 167.1 — Core theoryInternal Parametricity without an Interval
- Definition 167.2 — Spans and their operationsInternal Parametricity without an Interval
- Definition 167.3 — Equations of the span calculusInternal Parametricity without an Interval
- Definition 167.4 — Products and the universeInternal Parametricity without an Interval
- Definition 167.8 — Global theoryInternal Parametricity without an Interval
- Definition 167.10 — The cube categoryInternal Parametricity without an Interval
- Definition 167.13 — The gluing modelInternal Parametricity without an Interval
- Definition 168.1 — Types and termsReversible Classical Computation
- Definition 168.2 — TypingReversible Classical Computation
- Definition 168.3 — OrthogonalityReversible Classical Computation
- Definition 168.4 — Forward evaluationReversible Classical Computation
- Definition 168.8 — Syntactic inversionReversible Classical Computation
- Definition 168.12 — Backward evaluationReversible Classical Computation
- Definition 168.14 — Lists and a controlled negationReversible Classical Computation
- Definition 168.17 — Ancillae and uncomputationReversible Classical Computation
- Definition 168.19 — Partial injectionsReversible Classical Computation
- Definition 168.21 — Trace, following Joyal, Street and VerityReversible Classical Computation
- Definition 168.26 — Interpretation in PInjReversible Classical Computation
- Definition 169.1 — Concrete lens and its lawsProfunctors, Coends, and Optics
- Definition 169.5 — ProfunctorProfunctors, Coends, and Optics
- Definition 169.7 — Strength for an accessor shapeProfunctors, Coends, and Optics
- Definition 169.9 — Dinatural transformationProfunctors, Coends, and Optics
- Definition 169.10 — End and coendProfunctors, Coends, and Optics
- Definition 169.13 — Monoidal actionProfunctors, Coends, and Optics
- Definition 169.16 — OpticProfunctors, Coends, and Optics
- Definition 169.21 — The category of Tambara modulesProfunctors, Coends, and Optics
- Definition 169.22 — The generated Tambara moduleProfunctors, Coends, and Optics
- Definition 169.27 — Lawful opticProfunctors, Coends, and Optics
- Definition 169.32 — The traversal actionProfunctors, Coends, and Optics
- Definition 170.1 — Dependent lens over a familyDependent Optics and Indexed Bidirectional Structure
- Definition 170.4 — Dependent opticDependent Optics and Indexed Bidirectional Structure
- Definition 170.5 — Identity and compositionDependent Optics and Indexed Bidirectional Structure
- Definition 170.10 — The span bicategory and dependent lensesDependent Optics and Indexed Bidirectional Structure
- Definition 170.15 — Tambara representationDependent Optics and Indexed Bidirectional Structure
- Definition 170.16 — The universal representationDependent Optics and Indexed Bidirectional Structure
- Definition 171.2 — Deterministic contractionProbabilistic Lambda Calculi and Program Equivalence
- Definition 171.3 — Weak probabilistic reductionProbabilistic Lambda Calculi and Program Equivalence
- Definition 171.6 — The reduction matrixProbabilistic Lambda Calculi and Program Equivalence
- Definition 171.8 — Convergence probabilityProbabilistic Lambda Calculi and Program Equivalence
- Definition 171.12 — Observation contextsProbabilistic Lambda Calculi and Program Equivalence
- Definition 171.13 — Observational equivalenceProbabilistic Lambda Calculi and Program Equivalence
- Definition 171.14 — TestsProbabilistic Lambda Calculi and Program Equivalence
- Definition 171.17 — OrthogonalityProbabilistic Lambda Calculi and Program Equivalence
- Definition 171.19 — Probabilistic coherence spaceProbabilistic Lambda Calculi and Program Equivalence
- Definition 171.22 — Multisets and monomialsProbabilistic Lambda Calculi and Program Equivalence
- Definition 171.23 — The function form of a matrix, and the arrowProbabilistic Lambda Calculi and Program Equivalence
- Definition 171.29 — Interpretation of termsProbabilistic Lambda Calculi and Program Equivalence
- Definition 171.34 — The adequacy relationProbabilistic Lambda Calculi and Program Equivalence
- Definition 171.42 — Auxiliary programsProbabilistic Lambda Calculi and Program Equivalence
- Definition 171.43 — Counters and testing termsProbabilistic Lambda Calculi and Program Equivalence
- Definition 172.1 — Finite distributionProbability, Measure, Kernels, and Computable Sampling
- Definition 172.3 — Bit-stream sampler for the fragmentProbability, Measure, Kernels, and Computable Sampling
- Definition 172.6 — Measurable space and measurable mapProbability, Measure, Kernels, and Computable Sampling
- Definition 172.9 — Measure, subprobability, DiracProbability, Measure, Kernels, and Computable Sampling
- Definition 172.10 — PushforwardProbability, Measure, Kernels, and Computable Sampling
- Definition 172.16 — KernelProbability, Measure, Kernels, and Computable Sampling
- Definition 172.23 — Pointwise orderProbability, Measure, Kernels, and Computable Sampling
- Definition 172.28 — The fair-bit measure and its splittingProbability, Measure, Kernels, and Computable Sampling
- Definition 172.31 — Sampler and its pushforward measureProbability, Measure, Kernels, and Computable Sampling
- Definition 173.1 — Elementary conditioningComputable Conditioning and Its Limits
- Definition 173.3 — Conditional distributionComputable Conditioning and Its Limits
- Definition 173.8 — Conditioning operatorComputable Conditioning and Its Limits
- Definition 174.6 — Quasi-Borel spaceContinuous Probabilistic Languages and Quasi-Borel Semantics
- Definition 174.12 — Measures on a quasi-Borel spaceContinuous Probabilistic Languages and Quasi-Borel Semantics
- Definition 174.14 — Unit and bindContinuous Probabilistic Languages and Quasi-Borel Semantics
- Definition 175.2 — Mass functionsInference as Semantics-Preserving Program Transformation
- Definition 175.4 — Inference representationInference as Semantics-Preserving Program Transformation
- Definition 175.7 — Inference transformationInference as Semantics-Preserving Program Transformation
- Definition 175.13 — Inference transformerInference as Semantics-Preserving Program Transformation
- Definition 175.14 — The three transformersInference as Semantics-Preserving Program Transformation
- Definition 176.2 — The programming fragmentProbabilistic Program Logics
- Definition 176.3 — AssertionsProbabilistic Program Logics
- Definition 176.4 — The three judgmentsProbabilistic Program Logics
- Definition 176.6 — Probabilistic rulesProbabilistic Program Logics
- Definition 177.4 — The probabilistic rulesExpected Cost and Probabilistic Resource Analysis
- Definition 177.7 — Trace semanticsExpected Cost and Probabilistic Resource Analysis
- Definition 177.9 — Indexed distribution semanticsExpected Cost and Probabilistic Resource Analysis
- Definition 177.12 — Partial evaluation and its orderExpected Cost and Probabilistic Resource Analysis
- Definition 178.2 — The credit interfaceError Credits and Approximate Higher-Order Reasoning
- Definition 178.3 — The sampling rulesError Credits and Approximate Higher-Order Reasoning
- Definition 178.6 — Finite credit derivationsError Credits and Approximate Higher-Order Reasoning
- Definition 178.9 — The credit resource algebraError Credits and Approximate Higher-Order Reasoning
- Definition 179.2 — DensityVerified Compilation of Probabilistic Programs
- Definition 179.8 — Density judgmentVerified Compilation of Probabilistic Programs
- Definition 179.11 — Target expressions and the refinement invariantVerified Compilation of Probabilistic Programs
- Definition 180.2 — Families of measures and their reindexingDependent Probability and Fibred Measure
- Definition 180.6 — Quasi-Borel familyDependent Probability and Fibred Measure
- Definition 180.8 — Reindexing and comprehensionDependent Probability and Fibred Measure
- Definition 180.11 — The fibred distribution and probability familiesDependent Probability and Fibred Measure
- Definition 181.1 — Differential termsDifferential Lambda Calculus and Resource Taylor Expansion
- Definition 181.2 — Partial derivativeDifferential Lambda Calculus and Resource Taylor Expansion
- Definition 181.4 — Differential reductionDifferential Lambda Calculus and Resource Taylor Expansion
- Definition 181.6 — Simple resource terms and poly-termsDifferential Lambda Calculus and Resource Taylor Expansion
- Definition 181.7 — Differential substitutionDifferential Lambda Calculus and Resource Taylor Expansion
- Definition 181.9 — Resource reductionDifferential Lambda Calculus and Resource Taylor Expansion
- Definition 181.11 — SizeDifferential Lambda Calculus and Resource Taylor Expansion
- Definition 181.17 — MultiplicityDifferential Lambda Calculus and Resource Taylor Expansion
- Definition 181.18 — Taylor expansionDifferential Lambda Calculus and Resource Taylor Expansion
- Definition 181.21 — Coherence and uniform termsDifferential Lambda Calculus and Resource Taylor Expansion
- Definition 181.25 — B"ohm treeDifferential Lambda Calculus and Resource Taylor Expansion
- Definition 182.1 — Tangent pairingDifferentiable Semantics and Forward-Mode Automatic Differentiation
- Definition 182.4 — Types and termsDifferentiable Semantics and Forward-Mode Automatic Differentiation
- Definition 182.5 — Set-theoretic denotationDifferentiable Semantics and Forward-Mode Automatic Differentiation
- Definition 182.6 — The macro DDifferentiable Semantics and Forward-Mode Automatic Differentiation
- Definition 182.10 — The tangent relationDifferentiable Semantics and Forward-Mode Automatic Differentiation
- Definition 183.1 — The first-order source fragmentReverse-Mode Automatic Differentiation and Cotangent Semantics
- Definition 183.2 — Cotangent spacesReverse-Mode Automatic Differentiation and Cotangent Semantics
- Definition 183.3 — BackpropagatorReverse-Mode Automatic Differentiation and Cotangent Semantics
- Definition 183.4 — The reverse macroReverse-Mode Automatic Differentiation and Cotangent Semantics
- Definition 184.1 — Qubits and registersQuantum Lambda Calculi and Linear Quantum Data
- Definition 184.5 — MeasurementQuantum Lambda Calculi and Linear Quantum Data
- Definition 184.6 — Density matrices and channelsQuantum Lambda Calculi and Linear Quantum Data
- Definition 184.8 — Terms, values, and program statesQuantum Lambda Calculi and Linear Quantum Data
- Definition 184.9 — Probabilistic reductionQuantum Lambda Calculi and Linear Quantum Data
- Definition 184.10 — Types and subtypingQuantum Lambda Calculi and Linear Quantum Data
- Definition 184.11 — TypingQuantum Lambda Calculi and Linear Quantum Data
- Definition 184.13 — Error stateQuantum Lambda Calculi and Linear Quantum Data
- Definition 184.22 — Skeleton and liftingQuantum Lambda Calculi and Linear Quantum Data
- Definition 184.25 — Symmetric monoidal categoryQuantum Lambda Calculi and Linear Quantum Data
- Definition 184.27 — Compact closureQuantum Lambda Calculi and Linear Quantum Data
- Definition 184.29 — Dagger and dagger compactnessQuantum Lambda Calculi and Linear Quantum Data
- Definition 185.1 — TypesTyped Quantum Circuits and Proto-Quipper-M
- Definition 185.2 — Terms, values, and configurationsTyped Quantum Circuits and Proto-Quipper-M
- Definition 185.3 — Labelled circuitsTyped Quantum Circuits and Proto-Quipper-M
- Definition 185.4 — The two circuit operationsTyped Quantum Circuits and Proto-Quipper-M
- Definition 185.5 — Circuit generationTyped Quantum Circuits and Proto-Quipper-M
- Definition 185.8 — Well-typed configurationTyped Quantum Circuits and Proto-Quipper-M
- Definition 186.1 — SyntaxLinear-Dependent Quantum Programming and Proto-Quipper-D
- Definition 186.2 — ShapeLinear-Dependent Quantum Programming and Proto-Quipper-D
- Definition 186.3 — Selected typing rulesLinear-Dependent Quantum Programming and Proto-Quipper-D
- Definition 186.7 — Wire vectorsLinear-Dependent Quantum Programming and Proto-Quipper-D
- Definition 187.1 — Topological spaceElementary Topology and Classical Homotopy
- Definition 187.3 — Continuity, homeomorphismElementary Topology and Classical Homotopy
- Definition 187.6 — Product topologyElementary Topology and Classical Homotopy
- Definition 187.9 — ConnectednessElementary Topology and Classical Homotopy
- Definition 187.12 — Compactness, Hausdorff spacesElementary Topology and Classical Homotopy
- Definition 187.16 — Paths and loopsElementary Topology and Classical Homotopy
- Definition 187.18 — HomotopyElementary Topology and Classical Homotopy
- Definition 187.23 — Homotopy equivalenceElementary Topology and Classical Homotopy
- Definition 187.24 — Deformation retractionElementary Topology and Classical Homotopy
- Definition 187.29 — Pointed spacesElementary Topology and Classical Homotopy
- Definition 187.30 — Loop spaceElementary Topology and Classical Homotopy
- Definition 187.32 — Quotient topologyElementary Topology and Classical Homotopy
- Definition 187.34 — Disjoint union and pushoutElementary Topology and Classical Homotopy
- Definition 187.36 — Wedge, cone, suspension, mapping coneElementary Topology and Classical Homotopy
- Definition 187.41 — Standard simplexElementary Topology and Classical Homotopy
- Definition 188.1 — Covering mapFibrations, Homotopy Groups, and Exact Sequences
- Definition 188.8 — Fundamental groupFibrations, Homotopy Groups, and Exact Sequences
- Definition 188.10 — Induced homomorphism, change of base pointFibrations, Homotopy Groups, and Exact Sequences
- Definition 188.15 — Homotopy lifting property, fibrationFibrations, Homotopy Groups, and Exact Sequences
- Definition 188.18 — Homotopy groupsFibrations, Homotopy Groups, and Exact Sequences
- Definition 62.9 — Paths over a pathTypes as ∞-Groupoids
- Definition 62.10 — HomotopyTypes as ∞-Groupoids
- Definition 62.15 — Loop spacesTypes as ∞-Groupoids
- Definition 62.18 — FibreTypes as ∞-Groupoids
- Definition 62.19 — ContractibilityTypes as ∞-Groupoids
- Definition 62.21 — EquivalenceTypes as ∞-Groupoids
- Definition 62.23 — Quasi-inverseTypes as ∞-Groupoids
- Definition 189.43 — Propositions and setsTypes as ∞-Groupoids
- Definition 190.1 — Simplex categorySimplicial Sets, Horns, and Kan Fibrations
- Definition 190.2 — Cofaces and codegeneraciesSimplicial Sets, Horns, and Kan Fibrations
- Definition 190.5 — Simplicial setSimplicial Sets, Horns, and Kan Fibrations
- Definition 190.10 — Boundary and hornsSimplicial Sets, Horns, and Kan Fibrations
- Definition 190.13 — Kan conditionSimplicial Sets, Horns, and Kan Fibrations
- Definition 190.20 — Homotopy of simplicial maps and of verticesSimplicial Sets, Horns, and Kan Fibrations
- Definition 190.22 — ComponentsSimplicial Sets, Horns, and Kan Fibrations
- Definition 65.6 — UnivalenceUnivalence
- Definition 65.12 — Extensionality principlesUnivalence
- Definition 65.26 — Propositions and universes of propositionsUnivalence
- Definition 66.2 — Truncation levelsTruncation Levels, Propositions, and Logic
- Definition 66.4 — Propositions and setsTruncation Levels, Propositions, and Logic
- Definition 66.17 — EmbeddingTruncation Levels, Propositions, and Logic
- Definition 66.24Truncation Levels, Propositions, and Logic
- Definition 66.28 — Decidable equalityTruncation Levels, Propositions, and Logic
- Definition 66.33 — Propositional truncationTruncation Levels, Propositions, and Logic
- Definition 66.39 — Logical translationTruncation Levels, Propositions, and Logic
- Definition 66.42 — Excluded middleTruncation Levels, Propositions, and Logic
- Definition 66.46 — Axiom of choiceTruncation Levels, Propositions, and Logic
- Definition 66.52 — n-truncationTruncation Levels, Propositions, and Logic
- Definition 68.1 — Dependent paths and dependent 2-pathsHigher Inductive Types and Homotopy-Initiality
- Definition 68.8 — The circleHigher Inductive Types and Homotopy-Initiality
- Definition 198.15 — Circle algebras and homotopy-initialityHigher Inductive Types and Homotopy-Initiality
- Definition 68.15 — The intervalHigher Inductive Types and Homotopy-Initiality
- Definition 68.19 — SuspensionHigher Inductive Types and Homotopy-Initiality
- Definition 68.21 — SpheresHigher Inductive Types and Homotopy-Initiality
- Definition 68.22 — Pointed types, based maps, loop spacesHigher Inductive Types and Homotopy-Initiality
- Definition 68.26 — PushoutsHigher Inductive Types and Homotopy-Initiality
- Definition 68.27 — CoconesHigher Inductive Types and Homotopy-Initiality
- Definition 68.31 — Propositional truncation as a HITHigher Inductive Types and Homotopy-Initiality
- Definition 68.33 — Set truncationHigher Inductive Types and Homotopy-Initiality
- Definition 68.38 — Set quotientsHigher Inductive Types and Homotopy-Initiality
- Definition 69.2 — Pointed types and mapsCoverings, van Kampen, and the Fundamental Group
- Definition 69.4 — Homotopy groupsCoverings, van Kampen, and the Fundamental Group
- Definition 69.17 — Universal cover of the circleCoverings, van Kampen, and the Fundamental Group
- Definition 202.28 — Set-valued coveringsCoverings, van Kampen, and the Fundamental Group
- Definition 202.34 — Alternating-word free productCoverings, van Kampen, and the Fundamental Group
- Definition 74.2 — PrecategoryUnivalent Categories and Rezk Completion
- Definition 74.3 — IsomorphismUnivalent Categories and Rezk Completion
- Definition 74.6 — Univalent categoryUnivalent Categories and Rezk Completion
- Definition 74.12 — FunctorUnivalent Categories and Rezk Completion
- Definition 74.13 — Natural transformationUnivalent Categories and Rezk Completion
- Definition 74.15 — Functor precategoryUnivalent Categories and Rezk Completion
- Definition 74.18Univalent Categories and Rezk Completion
- Definition 74.19Univalent Categories and Rezk Completion
- Definition 74.24Univalent Categories and Rezk Completion
- Definition 74.29Univalent Categories and Rezk Completion
- Definition 74.30 — Yoneda embeddingUnivalent Categories and Rezk Completion
- Definition 74.42 — Notion of structureUnivalent Categories and Rezk Completion
- Definition 74.45 — Group structureUnivalent Categories and Rezk Completion
- Definition 74.48 — CardinalsSet-Level Mathematics in Univalent Foundations
- Definition 74.50Set-Level Mathematics in Univalent Foundations
- Definition 74.53 — AccessibilitySet-Level Mathematics in Univalent Foundations
- Definition 74.56 — OrdinalsSet-Level Mathematics in Univalent Foundations
- Definition 74.58 — SimulationSet-Level Mathematics in Univalent Foundations
- Definition 74.62 — Dedekind realsCompletions and the Real Numbers
- Definition 74.64Completions and the Real Numbers
- Definition 74.66 — Cauchy approximationCompletions and the Real Numbers
- Definition 74.68 — Cauchy realsChoice-Free HII Cauchy Completion
- Definition 79.1 — Strict propositionsObservational Equality and Computational Extensionality
- Definition 79.3 — Propositional formersObservational Equality and Computational Extensionality
- Definition 79.8 — The observational primitivesObservational Equality and Computational Extensionality
- Definition 79.11 — Observational equality: the computation tableObservational Equality and Computational Extensionality
- Definition 79.17 — Cast computationObservational Equality and Computational Extensionality
- Definition 79.22 — Quotient typesObservational Equality and Computational Extensionality
- Definition 79.24 — The 2007 observational theory, sketchObservational Equality and Computational Extensionality
- Definition 80.1 — The intervalCubical Type Theory I: De Morgan Cubes
- Definition 80.4 — Dimension contextsCubical Type Theory I: De Morgan Cubes
- Definition 80.8 — Path typesCubical Type Theory I: De Morgan Cubes
- Definition 80.14 — The face latticeCubical Type Theory I: De Morgan Cubes
- Definition 80.15 — Restricted contextsCubical Type Theory I: De Morgan Cubes
- Definition 80.18 — SystemsCubical Type Theory I: De Morgan Cubes
- Definition 80.21 — CompositionCubical Type Theory I: De Morgan Cubes
- Definition 80.25 — Composition computed by casesCubical Type Theory I: De Morgan Cubes
- Definition 80.31 — Cubical equivalencesCubical Type Theory I: De Morgan Cubes
- Definition 80.35 — Glue typesCubical Type Theory I: De Morgan Cubes
- Definition 80.39 — The cubical universeCubical Type Theory I: De Morgan Cubes
- Definition 80.41 — Composition for the universeCubical Type Theory I: De Morgan Cubes
- Definition 81.2 — The Cartesian intervalCubical Type Theory II: Cartesian Cubes and Computation
- Definition 81.4 — Cartesian cofibrationsCubical Type Theory II: Cartesian Cubes and Computation
- Definition 81.7 — Cartesian Kan operationsCubical Type Theory II: Cartesian Cubes and Computation
- Definition 81.22 — V-typesCubical Type Theory II: Cartesian Cubes and Computation
- Definition 81.27 — Cubical programsCubical Type Theory II: Cartesian Cubes and Computation
- Definition 81.28 — Judgments as behaviors; schematicCubical Type Theory II: Cartesian Cubes and Computation
- Definition 3Computational type theory, elaboration, and clause compilation
- Definition 4Computational type theory, elaboration, and clause compilation
- Definition 5Computational type theory, elaboration, and clause compilation
- Definition 6Computational type theory, elaboration, and clause compilation
- Definition 7Computational type theory, elaboration, and clause compilation