Lectures onType Theory
Theorems and results
Scholarly index

Theorems and results

  1. Proposition 1.5Judgments, Derivations, and Operational Semantics
  2. Proposition 1.10 — Structural recursion on syntaxJudgments, Derivations, and Operational Semantics
  3. Proposition 1.13Judgments, Derivations, and Operational Semantics
  4. Proposition 1.14 — Enumeration of derivationsJudgments, Derivations, and Operational Semantics
  5. Theorem 1.15 — Rule inductionJudgments, Derivations, and Operational Semantics
  6. Proposition 1.16 — Strengthened rule inductionJudgments, Derivations, and Operational Semantics
  7. Lemma 1.17 — PredecessorJudgments, Derivations, and Operational Semantics
  8. Lemma 1.18 — Symmetry of numeral equalityJudgments, Derivations, and Operational Semantics
  9. Lemma 1.23 — ParityJudgments, Derivations, and Operational Semantics
  10. Lemma 1.24 — Parity expressions are numeralsJudgments, Derivations, and Operational Semantics
  11. Lemma 1.25 — Disjointness of parityJudgments, Derivations, and Operational Semantics
  12. Lemma 1.27 — Subjects of addition are numeralsJudgments, Derivations, and Operational Semantics
  13. Proposition 1.28 — Addition is totalJudgments, Derivations, and Operational Semantics
  14. Lemma 1.29 — Addition is single-valuedJudgments, Derivations, and Operational Semantics
  15. Proposition 1.31 — Structural propertiesJudgments, Derivations, and Operational Semantics
  16. Theorem 1.34Judgments, Derivations, and Operational Semantics
  17. Proposition 1.35 — Admissibility is conservative one-rule extensionJudgments, Derivations, and Operational Semantics
  18. Lemma 1.37 — The two numeral judgments coincideJudgments, Derivations, and Operational Semantics
  19. Lemma 1.39 — Numerals do not stepJudgments, Derivations, and Operational Semantics
  20. Theorem 1.40 — DeterminismJudgments, Derivations, and Operational Semantics
  21. Lemma 1.42 — Transitivity of many stepsJudgments, Derivations, and Operational Semantics
  22. Lemma 1.44 — Big-step results are numeralsJudgments, Derivations, and Operational Semantics
  23. Lemma 1.45 — Numerals evaluate to themselvesJudgments, Derivations, and Operational Semantics
  24. Lemma 1.46 — Congruence for many stepsJudgments, Derivations, and Operational Semantics
  25. Lemma 1.47 — Numeral addition reducesJudgments, Derivations, and Operational Semantics
  26. Theorem 1.48 — Big step implies small stepsJudgments, Derivations, and Operational Semantics
  27. Proposition 1.49 — Arithmetic always advances or is a numeralJudgments, Derivations, and Operational Semantics
  28. Lemma 1.52 — Fresh-renaming equationsJudgments, Derivations, and Operational Semantics
  29. Lemma 1.54 — Alpha compatibility and common openingsJudgments, Derivations, and Operational Semantics
  30. Proposition 1.55 — Alpha-equivalence is an equivalence relationJudgments, Derivations, and Operational Semantics
  31. Lemma 1.56 — Fresh representatives and common openingJudgments, Derivations, and Operational Semantics
  32. Lemma 1.59 — Fresh opening commutes with substitutionJudgments, Derivations, and Operational Semantics
  33. Proposition 1.60 — Substitution is well definedJudgments, Derivations, and Operational Semantics
  34. Lemma 1.63 — Fresh-opening cancellationJudgments, Derivations, and Operational Semantics
  35. Proposition 1.66 — Raw judgments respect alpha-equivalenceJudgments, Derivations, and Operational Semantics
  36. Lemma 1.64 — One-step inclusion and many-step transitivityJudgments, Derivations, and Operational Semantics
  37. Lemma 1.65 — Arithmetic rules embed in the enlarged dynamicsJudgments, Derivations, and Operational Semantics
  38. Lemma 1.66 — Values are finalJudgments, Derivations, and Operational Semantics
  39. Lemma 1.69 — Unique decompositionJudgments, Derivations, and Operational Semantics
  40. Theorem 1.70 — Determinism of call-by-value reductionJudgments, Derivations, and Operational Semantics
  41. Lemma 1.72 — Full big-step results are valuesJudgments, Derivations, and Operational Semantics
  42. Lemma 1.73 — Agreement on arithmetic expressionsJudgments, Derivations, and Operational Semantics
  43. Lemma 1.74 — Many-step congruenceJudgments, Derivations, and Operational Semantics
  44. Theorem 1.75 — Big step implies small stepsJudgments, Derivations, and Operational Semantics
  45. Corollary 1.81 — Stuck terms do not evaluateJudgments, Derivations, and Operational Semantics
  46. Lemma 1.82 — A value evaluates only to itselfJudgments, Derivations, and Operational Semantics
  47. Lemma 1.83 — One-step expansion of big-step evaluationJudgments, Derivations, and Operational Semantics
  48. Theorem 1.84 — Small steps to a value imply big-step evaluationJudgments, Derivations, and Operational Semantics
  49. Corollary 1.85 — Agreement of full big-step and small-step evaluationJudgments, Derivations, and Operational Semantics
  50. Lemma 1.76 — Fresh renaming commutes with substitutionJudgments, Derivations, and Operational Semantics
  51. Lemma 1.77 — Renaming evaluation derivationsJudgments, Derivations, and Operational Semantics
  52. Lemma 1.78 — Substitution of evaluation derivationsJudgments, Derivations, and Operational Semantics
  53. Proposition 2.8 — The stuck term is untypableSimple Types, Curry–Howard, Safety, and Normalization
  54. Lemma 2.9 — RenamingSimple Types, Curry–Howard, Safety, and Normalization
  55. Corollary 2.10 — Opening an abstractionSimple Types, Curry–Howard, Safety, and Normalization
  56. Corollary 2.11 — Typing respects alpha-equivalenceSimple Types, Curry–Howard, Safety, and Normalization
  57. Lemma 2.13 — ScopeSimple Types, Curry–Howard, Safety, and Normalization
  58. Lemma 2.14 — WeakeningSimple Types, Curry–Howard, Safety, and Normalization
  59. Corollary 2.15 — Weakening by a telescopeSimple Types, Curry–Howard, Safety, and Normalization
  60. Theorem 2.16 — SubstitutionSimple Types, Curry–Howard, Safety, and Normalization
  61. Lemma 2.18 — InversionSimple Types, Curry–Howard, Safety, and Normalization
  62. Lemma 2.19 — Uniqueness of typesSimple Types, Curry–Howard, Safety, and Normalization
  63. Proposition 2.20 — Type synthesisSimple Types, Curry–Howard, Safety, and Normalization
  64. Lemma 2.22 — Canonical formsSimple Types, Curry–Howard, Safety, and Normalization
  65. Theorem 2.23 — PreservationSimple Types, Curry–Howard, Safety, and Normalization
  66. Theorem 2.24 — ProgressSimple Types, Curry–Howard, Safety, and Normalization
  67. Corollary 2.25 — Type safetySimple Types, Curry–Howard, Safety, and Normalization
  68. Proposition 2.29 — Structural metatheory survives the extensionSimple Types, Curry–Howard, Safety, and Normalization
  69. Lemma 2.35 — Extended canonical formsSimple Types, Curry–Howard, Safety, and Normalization
  70. Theorem 2.31 — Safety for the propositional extensionSimple Types, Curry–Howard, Safety, and Normalization
  71. Proposition 2.33 — Natural deduction is typingSimple Types, Curry–Howard, Safety, and Normalization
  72. Theorem 2.37 — Subject reductionSimple Types, Curry–Howard, Safety, and Normalization
  73. Corollary 2.44 — Many-step subject reductionSimple Types, Curry–Howard, Safety, and Normalization
  74. Lemma 2.47 — Finite reduction heightSimple Types, Curry–Howard, Safety, and Normalization
  75. Lemma 2.40 — SaturationSimple Types, Curry–Howard, Safety, and Normalization
  76. Lemma 2.50 — Fresh-renaming invarianceSimple Types, Curry–Howard, Safety, and Normalization
  77. Lemma 2.51 — Reduction and substitution compatibilitySimple Types, Curry–Howard, Safety, and Normalization
  78. Lemma 2.52 — Eliminator closureSimple Types, Curry–Howard, Safety, and Normalization
  79. Lemma 2.53 — Principal expansionSimple Types, Curry–Howard, Safety, and Normalization
  80. Theorem 2.42 — Fundamental lemmaSimple Types, Curry–Howard, Safety, and Normalization
  81. Theorem 2.43 — Strong normalizationSimple Types, Curry–Howard, Safety, and Normalization
  82. Lemma 2.57 — Machine steps are proof stepsSimple Types, Curry–Howard, Safety, and Normalization
  83. Corollary 2.58 — Call-by-value normalizationSimple Types, Curry–Howard, Safety, and Normalization
  84. Lemma 2.59 — Typed normal formsSimple Types, Curry–Howard, Safety, and Normalization
  85. Corollary 2.44 — ConsistencySimple Types, Curry–Howard, Safety, and Normalization
  86. Lemma 3.3 — First-order substitution lawsFirst-Order Proof Theory and Sequent Calculi
  87. Lemma 3.6 — Assignment agreement and semantic substitutionFirst-Order Proof Theory and Sequent Calculi
  88. Lemma 3.7 — Semantic soundness of natural deductionFirst-Order Proof Theory and Sequent Calculi
  89. Proposition 3.8 — Why the whole eigenvariable condition is necessaryFirst-Order Proof Theory and Sequent Calculi
  90. Lemma 3.9 — Freshening natural-deduction eigenvariablesFirst-Order Proof Theory and Sequent Calculi
  91. Corollary 3.10 — Prescribed outer natural-deduction eigenvariableFirst-Order Proof Theory and Sequent Calculi
  92. Lemma 3.11 — Weakening and individual substitutionFirst-Order Proof Theory and Sequent Calculi
  93. Lemma 3.13 — Freshening LJ eigenvariablesFirst-Order Proof Theory and Sequent Calculi
  94. Corollary 3.14 — Prescribed outer LJ eigenvariableFirst-Order Proof Theory and Sequent Calculi
  95. Lemma 3.15 — Semantic soundness of LJFirst-Order Proof Theory and Sequent Calculi
  96. Lemma 3.16 — Structural bookkeeping without cutFirst-Order Proof Theory and Sequent Calculi
  97. Lemma 3.17 — Split-context natural-deduction eliminationsFirst-Order Proof Theory and Sequent Calculi
  98. Theorem 3.18 — ND–LJ correspondenceFirst-Order Proof Theory and Sequent Calculi
  99. Lemma 3.20 — Principal cut reductionsFirst-Order Proof Theory and Sequent Calculi
  100. Lemma 3.22 — Multicut base casesFirst-Order Proof Theory and Sequent Calculi
  101. Lemma 3.23 — Commuting multicutsFirst-Order Proof Theory and Sequent Calculi
  102. Theorem 3.25 — Cut eliminationFirst-Order Proof Theory and Sequent Calculi
  103. Corollary 3.26 — Subformula property and consistencyFirst-Order Proof Theory and Sequent Calculi
  104. Corollary 3.27 — Disjunction and existence propertiesFirst-Order Proof Theory and Sequent Calculi
  105. Proposition 3.29 — First-order proof-term correspondenceFirst-Order Proof Theory and Sequent Calculi
  106. Lemma 3.31 — Normal-form characterizationFirst-Order Proof Theory and Sequent Calculi
  107. Lemma 3.32 — Neutral substitution preserves normalityFirst-Order Proof Theory and Sequent Calculi
  108. Lemma 3.33 — Cut-free back-translation is beta-normalFirst-Order Proof Theory and Sequent Calculi
  109. Theorem 3.34 — Normal inhabitationFirst-Order Proof Theory and Sequent Calculi
  110. Lemma 3.36 — Derived search rules and literal LJFirst-Order Proof Theory and Sequent Calculi
  111. Proposition 3.37 — Bounded-search correctnessFirst-Order Proof Theory and Sequent Calculi
  112. Lemma 4.6 — Extensionality of type substitutionHindley–Milner Type Inference
  113. Lemma 3.9 — Characterization of generalityHindley–Milner Type Inference
  114. Corollary 4.11 — Free variables decrease with generalityHindley–Milner Type Inference
  115. Lemma 3.10 — Stability of generalityHindley–Milner Type Inference
  116. Lemma 3.11 — Quantifier introductionHindley–Milner Type Inference
  117. Lemma 3.13 — MonotonicityHindley–Milner Type Inference
  118. Lemma 3.14 — Generalization under substitutionHindley–Milner Type Inference
  119. Lemma 3.15 — Fresh renaming before substitutionHindley–Milner Type Inference
  120. Lemma 3.18 — WeakeningHindley–Milner Type Inference
  121. Lemma 3.19 — Term substitutionHindley–Milner Type Inference
  122. Lemma 3.21 — Occurs checkHindley–Milner Type Inference
  123. Lemma 3.24 — TerminationHindley–Milner Type Inference
  124. Lemma 3.25 — Elimination factorizationHindley–Milner Type Inference
  125. Theorem 3.26 — Unification is sound and principalHindley–Milner Type Inference
  126. Corollary 4.31 — Mutual factorization of most general unifiersHindley–Milner Type Inference
  127. Lemma 4.35 — Completion of a finite name matchingHindley–Milner Type Inference
  128. Lemma 3.29 — Fresh-choice irrelevanceHindley–Milner Type Inference
  129. Lemma 3.32 — Type substitutionHindley–Milner Type Inference
  130. Lemma 3.33 — More general contextsHindley–Milner Type Inference
  131. Theorem 3.34 — Declarative and syntax-directed typing agreeHindley–Milner Type Inference
  132. Theorem 4.43 — Pure HM safetyHindley–Milner Type Inference
  133. Theorem 3.35 — Soundness of WHindley–Milner Type Inference
  134. Lemma 4.45 — Extending an MGU factorization off its problemHindley–Milner Type Inference
  135. Lemma 4.46 — Protected principal-pair inductionHindley–Milner Type Inference
  136. Theorem 3.36 — Principal-pair theoremHindley–Milner Type Inference
  137. Corollary 3.37 — Principal schemes in a closed signatureHindley–Milner Type Inference
  138. Corollary 4.49 — Principal generalization after an open-context runHindley–Milner Type Inference
  139. Lemma 4.52 — Evidence substitutionHindley–Milner Type Inference
  140. Lemma 4.53 — Evidence over a prescribed scopeHindley–Milner Type Inference
  141. Theorem 4.54 — Checked reconstruction from WHindley–Milner Type Inference
  142. Theorem 4.58 — Sound and principal list inferenceHindley–Milner Type Inference
  143. Lemma 4.64 — Context generality for value-restricted typingHindley–Milner Type Inference
  144. Lemma 4.65 — Value-restricted syntax equivalenceHindley–Milner Type Inference
  145. Lemma 4.66 — Protected induction for the value-restricted signatureHindley–Milner Type Inference
  146. Theorem 4.67 — Principality with the conservative value restrictionHindley–Milner Type Inference
  147. Lemma 4.69 — Run-time context generalityHindley–Milner Type Inference
  148. Lemma 4.70 — Run-time syntax equivalenceHindley–Milner Type Inference
  149. Lemma 4.71 — Run-time canonical formsHindley–Milner Type Inference
  150. Lemma 4.72 — Weakening by fresh store entriesHindley–Milner Type Inference
  151. Lemma 4.73 — Store-indexed value substitutionHindley–Milner Type Inference
  152. Theorem 3.40 — Safety with the value restrictionHindley–Milner Type Inference
  153. Proposition 5.3 — Equation encodingSemi-Unification and Polymorphic Recursion
  154. Lemma 5.4 — Finite-tree obstructionSemi-Unification and Polymorphic Recursion
  155. Theorem 5.8 — Local syntax-directed normalizationSemi-Unification and Polymorphic Recursion
  156. Lemma 5.9 — Mutual protected matching is renamingSemi-Unification and Polymorphic Recursion
  157. Lemma 5.10 — Scheme representationSemi-Unification and Polymorphic Recursion
  158. Theorem 5.12 — Constraint characterizationSemi-Unification and Polymorphic Recursion
  159. Corollary 5.14 — Forward reductionSemi-Unification and Polymorphic Recursion
  160. Lemma 5.15 — Representation and substitution correctnessSemi-Unification and Polymorphic Recursion
  161. Lemma 5.16 — Result-indexed Church formation and inversionSemi-Unification and Polymorphic Recursion
  162. Lemma 5.17 — Whole-encoder Church adequacySemi-Unification and Polymorphic Recursion
  163. Theorem 5.18 — Converse reductionSemi-Unification and Polymorphic Recursion
  164. Corollary 5.19 — Log-space equivalenceSemi-Unification and Polymorphic Recursion
  165. Lemma 5.21 — The one-tape source is r.e.-completeSemi-Unification and Polymorphic Recursion
  166. Lemma 5.22 — The one-tape source is undecidableSemi-Unification and Polymorphic Recursion
  167. Lemma 5.23 — Finite support for semi-unificationSemi-Unification and Polymorphic Recursion
  168. Lemma 5.24 — Machine-model bridgeSemi-Unification and Polymorphic Recursion
  169. Theorem 5.25 — Exact constructive reduction importSemi-Unification and Polymorphic Recursion
  170. Theorem 5.26 — Constructive semi-unification boundarySemi-Unification and Polymorphic Recursion
  171. Corollary 5.27 — UndecidabilitySemi-Unification and Polymorphic Recursion
  172. Lemma 6.2 — Dimension-group lawsDimension Types and Units of Measure
  173. Lemma 6.7 — Dimension typing is syntax-directedDimension Types and Units of Measure
  174. Lemma 6.8 — Dimension conversion preserves type shapeDimension Types and Units of Measure
  175. Lemma 6.9 — Two-entry gcd reductionDimension Types and Units of Measure
  176. Lemma 6.10 — Dividing pivotDimension Types and Units of Measure
  177. Lemma 6.11 — Smith reduction over the integersDimension Types and Units of Measure
  178. Theorem 6.13 — Dimension-solver soundness and principalityDimension Types and Units of Measure
  179. Corollary 6.14 — Integer-exponent Buckingham π countDimension Types and Units of Measure
  180. Lemma 6.15 — Composing principal dimension solvesDimension Types and Units of Measure
  181. Lemma 6.17 — Termination of dimension-aware unificationDimension Types and Units of Measure
  182. Theorem 6.18 — Mixed-unifier contractDimension Types and Units of Measure
  183. Theorem 6.21 — Principal dimension inferenceDimension Types and Units of Measure
  184. Lemma 6.25 — Elaboration typingDimension Types and Units of Measure
  185. Lemma 6.26 — Core substitution and numeric canonical formsDimension Types and Units of Measure
  186. Lemma 6.27 — Unique core decompositionDimension Types and Units of Measure
  187. Theorem 6.28 — Core preservation and progressDimension Types and Units of Measure
  188. Corollary 6.29 — Source dimensional safetyDimension Types and Units of Measure
  189. Lemma 6.31 — Saturation for dimension-core candidatesDimension Types and Units of Measure
  190. Lemma 6.32 — Fundamental lemma for the dimension coreDimension Types and Units of Measure
  191. Lemma 6.33 — Termination of the dimension coreDimension Types and Units of Measure
  192. Lemma 6.34 — One-step expansion of core evaluationDimension Types and Units of Measure
  193. Theorem 6.35 — Unit-change invarianceDimension Types and Units of Measure
  194. Lemma 7.6 — Formation and constructor separationRow Polymorphism and Extensible Records and Variants
  195. Lemma 4.4 — Lacks respects row equalityRow Polymorphism and Extensible Records and Variants
  196. Lemma 4.5 — Finite-map character of strict rowsRow Polymorphism and Extensible Records and Variants
  197. Lemma 7.12 — Predicate weakeningRow Polymorphism and Extensible Records and Variants
  198. Lemma 4.9 — Changing the predicate contextRow Polymorphism and Extensible Records and Variants
  199. Lemma 4.10 — Qualified typing respects equivalent contextsRow Polymorphism and Extensible Records and Variants
  200. Lemma 7.16 — Admissibility of one-variable eliminationRow Polymorphism and Extensible Records and Variants
  201. Lemma 4.11 — Identity and composition of admissible substitutionsRow Polymorphism and Extensible Records and Variants
  202. Lemma 4.12 — Ambient formation and generalized declarationsRow Polymorphism and Extensible Records and Variants
  203. Lemma 4.18 — Structural stabilityRow Polymorphism and Extensible Records and Variants
  204. Corollary 4.19 — Ground dischargeRow Polymorphism and Extensible Records and Variants
  205. Lemma 4.20 — Peeling and deletionRow Polymorphism and Extensible Records and Variants
  206. Lemma 4.21 — Ground canonical formsRow Polymorphism and Extensible Records and Variants
  207. Theorem 4.22 — Safety of strict records and variantsRow Polymorphism and Extensible Records and Variants
  208. Lemma 7.28 — Determinism of the extended sourceRow Polymorphism and Extensible Records and Variants
  209. Lemma 7.32 — Well-founded multiset descentRow Polymorphism and Extensible Records and Variants
  210. Lemma 4.25 — TerminationRow Polymorphism and Extensible Records and Variants
  211. Lemma 4.26 — Fresh support of insertion and solvingRow Polymorphism and Extensible Records and Variants
  212. Theorem 4.27 — Principal row solverRow Polymorphism and Extensible Records and Variants
  213. Lemma 7.38 — Fixed-choice determinism of qualified WRow Polymorphism and Extensible Records and Variants
  214. Lemma 4.30 — Fresh support of qualified WRow Polymorphism and Extensible Records and Variants
  215. Lemma 4.33 — Restricted-support transportRow Polymorphism and Extensible Records and Variants
  216. Lemma 4.34 — Qualified generalization calculationRow Polymorphism and Extensible Records and Variants
  217. Theorem 4.35 — Sound, complete, principal row inferenceRow Polymorphism and Extensible Records and Variants
  218. Lemma 4.37 — Evidence coherenceRow Polymorphism and Extensible Records and Variants
  219. Lemma 7.49 — Canonical target indicesRow Polymorphism and Extensible Records and Variants
  220. Lemma 4.43 — The six offset simulationsRow Polymorphism and Extensible Records and Variants
  221. Lemma 4.44 — Typing of evidence elaborationRow Polymorphism and Extensible Records and Variants
  222. Lemma 4.45 — Fundamental evidence lemmaRow Polymorphism and Extensible Records and Variants
  223. Theorem 4.46 — Preservation, adequacy, and coherence of evidence passingRow Polymorphism and Extensible Records and Variants
  224. Corollary 7.61 — Coherent principal compilationRow Polymorphism and Extensible Records and Variants
  225. Lemma 8.3 — Formation and record-kind weakeningType-Preserving Compilation of Polymorphic Records
  226. Lemma 8.4 — Formation substitutionType-Preserving Compilation of Polymorphic Records
  227. Lemma 8.5 — Kinding substitutionType-Preserving Compilation of Polymorphic Records
  228. Lemma 8.10 — Totality and typing of numeral substitutionType-Preserving Compilation of Polymorphic Records
  229. Lemma 8.12 — Determinism and evaluation-prefix closureType-Preserving Compilation of Polymorphic Records
  230. Lemma 8.13 — Canonical translation and index transportType-Preserving Compilation of Polymorphic Records
  231. Lemma 8.15 — Index availabilityType-Preserving Compilation of Polymorphic Records
  232. Theorem 8.16 — Total and deterministic compilationType-Preserving Compilation of Polymorphic Records
  233. Theorem 8.17 — Type preservation of record compilationType-Preserving Compilation of Polymorphic Records
  234. Lemma 8.19 — Closing and compatibilityType-Preserving Compilation of Polymorphic Records
  235. Lemma 8.20 — Closing substitution equalityType-Preserving Compilation of Polymorphic Records
  236. Theorem 8.21 — Fundamental compilation relationType-Preserving Compilation of Polymorphic Records
  237. Corollary 8.22 — Semantic correctness at observable typesType-Preserving Compilation of Polymorphic Records
  238. Theorem 8.23 — Ohori's compilation theoremType-Preserving Compilation of Polymorphic Records
  239. Lemma 5.5 — Scope and weakeningSystem F, Impredicativity, and Normalization
  240. Lemma 5.6 — Type substitutionSystem F, Impredicativity, and Normalization
  241. Lemma 5.7 — Term substitutionSystem F, Impredicativity, and Normalization
  242. Lemma 5.9 — Canonical formsSystem F, Impredicativity, and Normalization
  243. Theorem 5.10 — PreservationSystem F, Impredicativity, and Normalization
  244. Theorem 5.11 — ProgressSystem F, Impredicativity, and Normalization
  245. Corollary 5.12 — SafetySystem F, Impredicativity, and Normalization
  246. Proposition 5.14 — Subject reduction for compatible betaSystem F, Impredicativity, and Normalization
  247. Theorem 5.21 — Erasure and decorationSystem F, Impredicativity, and Normalization
  248. Proposition 5.22 — Decidable Church checkingSystem F, Impredicativity, and Normalization
  249. Theorem 5.23 — Undecidability boundarySystem F, Impredicativity, and Normalization
  250. Lemma 5.26 — Elementary candidate constructionsSystem F, Impredicativity, and Normalization
  251. Lemma 9.28 — Candidate-component independenceSystem F, Impredicativity, and Normalization
  252. Lemma 5.28 — Interpretations are candidatesSystem F, Impredicativity, and Normalization
  253. Lemma 9.30 — Interpretation irrelevanceSystem F, Impredicativity, and Normalization
  254. Lemma 5.29 — Candidate substitutionSystem F, Impredicativity, and Normalization
  255. Lemma 5.32 — Reflection through a fresh substitutionSystem F, Impredicativity, and Normalization
  256. Lemma 5.30 — Term-abstraction expansionSystem F, Impredicativity, and Normalization
  257. Lemma 5.31 — Type-abstraction expansionSystem F, Impredicativity, and Normalization
  258. Theorem 5.34 — Fundamental theorem of reducibilitySystem F, Impredicativity, and Normalization
  259. Theorem 5.35 — Strong normalizationSystem F, Impredicativity, and Normalization
  260. Lemma 9.38 — Normal and neutral shapesSystem F, Impredicativity, and Normalization
  261. Corollary 5.36 — Syntactic consistencySystem F, Impredicativity, and Normalization
  262. Lemma 5.37 — Parallel substitutionSystem F, Impredicativity, and Normalization
  263. Lemma 9.42 — Parallel diamondSystem F, Impredicativity, and Normalization
  264. Lemma 9.43 — Sequentializing parallel reductionSystem F, Impredicativity, and Normalization
  265. Theorem 5.38 — Church–RosserSystem F, Impredicativity, and Normalization
  266. Corollary 9.45 — Conversion has a common reductSystem F, Impredicativity, and Normalization
  267. Proposition 5.39 — Closed normal booleans and naturalsSystem F, Impredicativity, and Normalization
  268. Lemma 9.49 — Functor laws for TSystem F, Impredicativity, and Normalization
  269. Theorem 9.50 — Imported stable-restriction interfaceSystem F, Impredicativity, and Normalization
  270. Lemma 9.51System F, Impredicativity, and Normalization
  271. Theorem 5.40 — Reynolds' set-theoretic obstructionSystem F, Impredicativity, and Normalization
  272. Lemma 5.41 — Normal iteratorsSystem F, Impredicativity, and Normalization
  273. Proposition 5.43 — Relational uniformity of iteratorsSystem F, Impredicativity, and Normalization
  274. Lemma 6.3 — Graph calculationRelational Parametricity and Abstraction Theorems
  275. Lemma 10.6 — Relational alpha-equivarianceRelational Parametricity and Abstraction Theorems
  276. Lemma 6.6 — Compatibility with beta-classesRelational Parametricity and Abstraction Theorems
  277. Lemma 6.7 — Endpoints and irrelevant variablesRelational Parametricity and Abstraction Theorems
  278. Lemma 6.8 — Relational type substitutionRelational Parametricity and Abstraction Theorems
  279. Theorem 6.10 — Abstraction theoremRelational Parametricity and Abstraction Theorems
  280. Corollary 6.11 — Self-parametricityRelational Parametricity and Abstraction Theorems
  281. Proposition 6.12 — The polymorphic endomap is pointwise the identityRelational Parametricity and Abstraction Theorems
  282. Corollary 10.15 — Unary preservationRelational Parametricity and Abstraction Theorems
  283. Corollary 6.13 — Parametric emptinessRelational Parametricity and Abstraction Theorems
  284. Proposition 6.14 — Identity extension at Church observationsRelational Parametricity and Abstraction Theorems
  285. Proposition 6.15 — Failure of unrestricted beta identity extensionRelational Parametricity and Abstraction Theorems
  286. Proposition 6.16 — Polymorphic applicationRelational Parametricity and Abstraction Theorems
  287. Theorem 6.17 — Iterator naturalityRelational Parametricity and Abstraction Theorems
  288. Theorem 6.18 — Counter representation independenceRelational Parametricity and Abstraction Theorems
  289. Proposition 10.23 — Least fixed points preserve strict admissible relationsRelational Parametricity and Abstraction Theorems
  290. Lemma 7.8 — Weakening and substitution for kindingType Operators, Kinds, and System F-omega
  291. Lemma 7.9 — Kinding inversion and uniquenessType Operators, Kinds, and System F-omega
  292. Lemma 11.12 — Term regularityType Operators, Kinds, and System F-omega
  293. Lemma 7.10 — Subject reduction for kindingType Operators, Kinds, and System F-omega
  294. Lemma 7.11 — Equality regularityType Operators, Kinds, and System F-omega
  295. Lemma 7.12 — Reduction is included in equalityType Operators, Kinds, and System F-omega
  296. Lemma 7.14 — Finite branching and reduction heightType Operators, Kinds, and System F-omega
  297. Lemma 7.16 — Properties of reducibilityType Operators, Kinds, and System F-omega
  298. Lemma 7.17 — Substitution and reductionType Operators, Kinds, and System F-omega
  299. Lemma 7.18 — AbstractionType Operators, Kinds, and System F-omega
  300. Lemma 7.19 — Formers preserve normalizationType Operators, Kinds, and System F-omega
  301. Lemma 7.20 — Fundamental lemma for kindingType Operators, Kinds, and System F-omega
  302. Theorem 7.21 — Type-level strong normalizationType Operators, Kinds, and System F-omega
  303. Lemma 7.22 — Local confluenceType Operators, Kinds, and System F-omega
  304. Theorem 7.23 — Confluence on normalizing constructorsType Operators, Kinds, and System F-omega
  305. Corollary 7.24 — Unique normal formsType Operators, Kinds, and System F-omega
  306. Theorem 7.25 — Conversion is common reductionType Operators, Kinds, and System F-omega
  307. Corollary 7.26 — The conversion facts required by term checkingType Operators, Kinds, and System F-omega
  308. Lemma 7.27 — Constructor equality respects substitutionType Operators, Kinds, and System F-omega
  309. Lemma 11.33 — Constructor equality weakeningType Operators, Kinds, and System F-omega
  310. Lemma 11.34 — Structural properties of F_ω term typingType Operators, Kinds, and System F-omega
  311. Lemma 7.28 — Stripping final conversionsType Operators, Kinds, and System F-omega
  312. Lemma 11.36 — Canonical forms for pure F_ωType Operators, Kinds, and System F-omega
  313. Theorem 11.37 — Pure-term preservationType Operators, Kinds, and System F-omega
  314. Theorem 11.38 — Pure-term progressType Operators, Kinds, and System F-omega
  315. Corollary 11.39 — Pure-term safetyType Operators, Kinds, and System F-omega
  316. Lemma 7.29 — Unicity of typing up to conversionType Operators, Kinds, and System F-omega
  317. Theorem 11.42 — Correctness of syntax-directed term inferenceType Operators, Kinds, and System F-omega
  318. Lemma 7.30 — Closed normal typesType Operators, Kinds, and System F-omega
  319. Lemma 7.33 — Structural lemmas for package termsExistential Types, Abstract Data, and Representation Independence
  320. Lemma 12.5 — Determinism of package evaluationExistential Types, Abstract Data, and Representation Independence
  321. Proposition 7.36 — Subject reduction for compatible term betaExistential Types, Abstract Data, and Representation Independence
  322. Lemma 7.37 — Canonical package valuesExistential Types, Abstract Data, and Representation Independence
  323. Theorem 7.38 — PreservationExistential Types, Abstract Data, and Representation Independence
  324. Theorem 7.39 — ProgressExistential Types, Abstract Data, and Representation Independence
  325. Corollary 7.40 — SafetyExistential Types, Abstract Data, and Representation Independence
  326. Lemma 12.14 — Constructor-convertible relation endpointsExistential Types, Abstract Data, and Representation Independence
  327. Lemma 7.45 — Endpoints and irrelevant constructor variablesExistential Types, Abstract Data, and Representation Independence
  328. Lemma 7.46 — Relational constructor substitutionExistential Types, Abstract Data, and Representation Independence
  329. Lemma 7.47 — Invariance under constructor equalityExistential Types, Abstract Data, and Representation Independence
  330. Theorem 7.48 — Abstraction for F_ω with existentialsExistential Types, Abstract Data, and Representation Independence
  331. Corollary 7.49 — Self-parametricityExistential Types, Abstract Data, and Representation Independence
  332. Corollary 12.23 — Related values are indistinguishable by natural clientsExistential Types, Abstract Data, and Representation Independence
  333. Lemma 7.50 — The counter packages are relatedExistential Types, Abstract Data, and Representation Independence
  334. Theorem 7.51 — Existential counter representation independenceExistential Types, Abstract Data, and Representation Independence
  335. Lemma 11.1 — Resolution terminates and is functionalQualified Types, Type Classes, and Coherent Dictionary Elaboration
  336. Lemma 11.2 — CanonicalizationQualified Types, Type Classes, and Coherent Dictionary Elaboration
  337. Lemma 13.8 — Canonical factorizationQualified Types, Type Classes, and Coherent Dictionary Elaboration
  338. Lemma 13.9 — Canonical environment actions composeQualified Types, Type Classes, and Coherent Dictionary Elaboration
  339. Lemma 11.3 — The generalization split is maximalQualified Types, Type Classes, and Coherent Dictionary Elaboration
  340. Lemma 13.11 — Declarative typing is stable under canonical substitutionQualified Types, Type Classes, and Coherent Dictionary Elaboration
  341. Theorem 11.4 — Inference soundnessQualified Types, Type Classes, and Coherent Dictionary Elaboration
  342. Theorem 11.5 — Success and principality for QTC_0Qualified Types, Type Classes, and Coherent Dictionary Elaboration
  343. Lemma 13.15 — Target substitution is scoped under mergingQualified Types, Type Classes, and Coherent Dictionary Elaboration
  344. Theorem 11.6 — Target type preservationQualified Types, Type Classes, and Coherent Dictionary Elaboration
  345. Lemma 13.17 — Core–target step correspondenceQualified Types, Type Classes, and Coherent Dictionary Elaboration
  346. Lemma 13.18 — Core dynamic preservation and value reflectionQualified Types, Type Classes, and Coherent Dictionary Elaboration
  347. Theorem 11.7 — Forward operational simulationQualified Types, Type Classes, and Coherent Dictionary Elaboration
  348. Theorem 11.8 — Algorithmic coherenceQualified Types, Type Classes, and Coherent Dictionary Elaboration
  349. Proposition 13.21 — Ground-table specializationQualified Types, Type Classes, and Coherent Dictionary Elaboration
  350. Theorem 13.23 — Soundness of associated-type inference—importedQualified Types, Type Classes, and Coherent Dictionary Elaboration
  351. Theorem 11.10 — Imported COCHIS boundaryQualified Types, Type Classes, and Coherent Dictionary Elaboration
  352. Proposition 14.1 — Decision for the singleton constructor fragmentML Modules: Abstraction, Functors, and Sharing
  353. Proposition 14.7 — Termination and soundness of algorithmic matchingML Modules: Abstraction, Functors, and Sharing
  354. Proposition 12.4 — Sharing preservationML Modules: Abstraction, Functors, and Sharing
  355. Lemma 14.15 — Projectible-witness coherenceML Modules: Abstraction, Functors, and Sharing
  356. Theorem 12.7 — Supported elaborationML Modules: Abstraction, Functors, and Sharing
  357. Lemma 14.17 — Operational values elaborate to target valuesML Modules: Abstraction, Functors, and Sharing
  358. Lemma 14.18 — Derivation substitutionML Modules: Abstraction, Functors, and Sharing
  359. Theorem 12.8 — Simulation and module safetyML Modules: Abstraction, Functors, and Sharing
  360. Lemma 12.10 — Counter fundamental relationML Modules: Abstraction, Functors, and Sharing
  361. Theorem 12.11 — Counter representation independenceML Modules: Abstraction, Functors, and Sharing
  362. Lemma 14.26 — Static shape of every principal basic componentML Modules: Abstraction, Functors, and Sharing
  363. Lemma 14.27 — NarrowingML Modules: Abstraction, Functors, and Sharing
  364. Lemma 14.28 — Structural matching inversionML Modules: Abstraction, Functors, and Sharing
  365. Corollary 14.29 — Decision and completeness of structural matchingML Modules: Abstraction, Functors, and Sharing
  366. Lemma 14.30 — Typing factorization for projectible pathsML Modules: Abstraction, Functors, and Sharing
  367. Theorem 12.13 — Principal matching for closed projectible valuesML Modules: Abstraction, Functors, and Sharing
  368. Theorem 14.32 — Phase-sensitive transport—importedML Modules: Abstraction, Functors, and Sharing
  369. Lemma 15.4 — Definedness grows exactly by writesMixML, Recursive Linking, and Definedness
  370. Lemma 15.5 — No read before definitionMixML, Recursive Linking, and Definedness
  371. Proposition 15.8 — Ordered slot-trace safetyMixML, Recursive Linking, and Definedness
  372. Theorem 15.12 — Full MixML/LTG theorem boundary; exact importMixML, Recursive Linking, and Definedness
  373. Lemma 16.4 — Compatible extensionModular Type Classes and Implicit Modules
  374. Theorem 16.6 — Exactness and uniqueness of MTC_0 resolutionModular Type Classes and Implicit Modules
  375. Corollary 16.7 — Resolution is stable under admissible extensionModular Type Classes and Implicit Modules
  376. Lemma 16.8 — Evidence embedding into the term contextModular Type Classes and Implicit Modules
  377. Proposition 16.9 — Type preservation of evidence insertionModular Type Classes and Implicit Modules
  378. Lemma 16.11 — Grounding residual evidenceModular Type Classes and Implicit Modules
  379. Theorem 16.14 — Imported: published inference soundnessModular Type Classes and Implicit Modules
  380. Theorem 16.17 — Published SI resultsModular Type Classes and Implicit Modules
  381. Lemma 17.1 — Mixed parallel substitution and diamondTyped Self-Representation in System F-omega
  382. Lemma 7.56 — Term normalization and confluence used hereTyped Self-Representation in System F-omega
  383. Proposition 7.57 — The normalization barrier, exactly statedTyped Self-Representation in System F-omega
  384. Lemma 7.59 — Typing and normality of shallow quotationTyped Self-Representation in System F-omega
  385. Theorem 7.60 — Strong shallow unquotingTyped Self-Representation in System F-omega
  386. Lemma 7.61 — Formation and substitution of type pre-representationsTyped Self-Representation in System F-omega
  387. Lemma 7.64 — Fundamental typing lemma for deep quotationTyped Self-Representation in System F-omega
  388. Lemma 7.65 — Fold calculationTyped Self-Representation in System F-omega
  389. Lemma 7.66 — Recovery of represented typesTyped Self-Representation in System F-omega
  390. Lemma 7.67 — Unquoting a prequotationTyped Self-Representation in System F-omega
  391. Theorem 7.68 — Strong typed self-interpretationTyped Self-Representation in System F-omega
  392. Corollary 7.69 — Separation of represented beta classesTyped Self-Representation in System F-omega
  393. Theorem 7.70 — Correctness of the abstraction testTyped Self-Representation in System F-omega
  394. Theorem 7.71 — Correctness of sizeTyped Self-Representation in System F-omega
  395. Lemma 17.19 — Normal applications have neutral operatorsTyped Self-Representation in System F-omega
  396. Lemma 7.73 — The three-state invariantTyped Self-Representation in System F-omega
  397. Theorem 7.74 — Correctness of the normal-form testTyped Self-Representation in System F-omega
  398. Proposition 8.3 — Why arrow domains reverseSubtyping, Records, and Bounded Quantification
  399. Lemma 18.6 — Top is maximal in the first-order calculusSubtyping, Records, and Bounded Quantification
  400. Lemma 8.5 — First-order subtype shapeSubtyping, Records, and Bounded Quantification
  401. Lemma 8.6 — Literal-record inversion through subsumptionSubtyping, Records, and Bounded Quantification
  402. Lemma 8.7 — Introduction inversion through subsumptionSubtyping, Records, and Bounded Quantification
  403. Lemma 8.8 — Canonical forms through subsumptionSubtyping, Records, and Bounded Quantification
  404. Lemma 8.9 — Weakening and term substitutionSubtyping, Records, and Bounded Quantification
  405. Theorem 8.10 — PreservationSubtyping, Records, and Bounded Quantification
  406. Theorem 8.11 — ProgressSubtyping, Records, and Bounded Quantification
  407. Corollary 8.12 — SafetySubtyping, Records, and Bounded Quantification
  408. Lemma 18.15 — The first-order subtype orderSubtyping, Records, and Bounded Quantification
  409. Theorem 18.18 — First-order types form a latticeSubtyping, Records, and Bounded Quantification
  410. Proposition 8.14 — Conditional record boundsSubtyping, Records, and Bounded Quantification
  411. Lemma 18.21 — Top is maximal in KernelSubtyping, Records, and Bounded Quantification
  412. Theorem 8.18 — Strengthened structural packageSubtyping, Records, and Bounded Quantification
  413. Lemma 8.19 — Universal subtype inversion in Kernel F_<:Subtyping, Records, and Bounded Quantification
  414. Lemma 8.20 — Concrete inversion in Kernel F_<:Subtyping, Records, and Bounded Quantification
  415. Lemma 18.27 — Type-abstraction inversion in KernelSubtyping, Records, and Bounded Quantification
  416. Corollary 8.21 — Safety of the bounded extensionSubtyping, Records, and Bounded Quantification
  417. Proposition 18.29 — Source-only promotionSubtyping, Records, and Bounded Quantification
  418. Theorem 8.23 — Algorithm terminationSubtyping, Records, and Bounded Quantification
  419. Lemma 8.24 — Algorithmic weakeningSubtyping, Records, and Bounded Quantification
  420. Lemma 8.25 — Algorithmic transitivity and narrowingSubtyping, Records, and Bounded Quantification
  421. Theorem 8.26 — Soundness and completeness of algorithmic subtypingSubtyping, Records, and Bounded Quantification
  422. Lemma 18.36 — Top is maximal in fullSubtyping, Records, and Bounded Quantification
  423. Theorem 8.29 — Undecidability of full F_<: subtyping; exact importSubtyping, Records, and Bounded Quantification
  424. Lemma 18.40 — Arrow shape in fullSubtyping, Records, and Bounded Quantification
  425. Lemma 18.41 — Lambda inversion in the full- arrow fragmentSubtyping, Records, and Bounded Quantification
  426. Corollary 8.30 — Undecidability of full-F_<: typecheckingSubtyping, Records, and Bounded Quantification
  427. Lemma 19.6 — Nonrecursive atomic elimination preserves instancesAlgebraic Subtyping and Principal Inference
  428. Lemma 19.7 — Guarded recursive atomic elimination preserves instancesAlgebraic Subtyping and Principal Inference
  429. Lemma 19.9 — One work-list step is equisatisfiableAlgebraic Subtyping and Principal Inference
  430. Theorem 19.11 — Local biunificationAlgebraic Subtyping and Principal Inference
  431. Theorem 19.13 — Principal inference for MLsub_0Algebraic Subtyping and Principal Inference
  432. Theorem 19.14 — Richer MLsub inference boundary; exact importAlgebraic Subtyping and Principal Inference
  433. Theorem 19.16 — Boolean comparison boundary; exact importAlgebraic Subtyping and Principal Inference
  434. Proposition 9.7 — Boolean laws and varianceIntersection, Union, and Semantic Subtyping
  435. Corollary 9.8 — Subtyping is emptinessIntersection, Union, and Semantic Subtyping
  436. Lemma 9.10 — DNF correctnessIntersection, Union, and Semantic Subtyping
  437. Lemma 9.11 — Product decompositionIntersection, Union, and Semantic Subtyping
  438. Lemma 9.12 — Arrow decompositionIntersection, Union, and Semantic Subtyping
  439. Lemma 20.11 — Basic-shape emptinessIntersection, Union, and Semantic Subtyping
  440. Lemma 9.14 — Simulation soundnessIntersection, Union, and Semantic Subtyping
  441. Lemma 9.15 — Simulation completenessIntersection, Union, and Semantic Subtyping
  442. Theorem 9.16 — Emptiness and semantic subtyping are decidableIntersection, Union, and Semantic Subtyping
  443. Lemma 9.21 — Strong disjunction for a function clauseIntersection, Union, and Semantic Subtyping
  444. Lemma 9.23 — Application-output characterizationIntersection, Union, and Semantic Subtyping
  445. Lemma 9.25 — Projection-output characterizationIntersection, Union, and Semantic Subtyping
  446. Lemma 9.27 — Structural rulesIntersection, Union, and Semantic Subtyping
  447. Lemma 9.29 — Exact value typingIntersection, Union, and Semantic Subtyping
  448. Lemma 9.30 — Value refinement and canonical formsIntersection, Union, and Semantic Subtyping
  449. Lemma 9.31 — Interface applicationIntersection, Union, and Semantic Subtyping
  450. Theorem 9.32 — PreservationIntersection, Union, and Semantic Subtyping
  451. Theorem 9.33 — Progress and safetyIntersection, Union, and Semantic Subtyping
  452. Lemma 20.37 — Synthesis soundnessIntersection, Union, and Semantic Subtyping
  453. Lemma 20.38 — Synthesis leastnessIntersection, Union, and Semantic Subtyping
  454. Theorem 9.35 — Checker characterizationIntersection, Union, and Semantic Subtyping
  455. Lemma 21.3 — Coercion typingDisjoint Intersections, Merge Elaboration, and Coherence
  456. Lemma 21.5 — Unique contributorDisjoint Intersections, Merge Elaboration, and Coherence
  457. Lemma 21.7 — Ordinary-leaf decompositionDisjoint Intersections, Merge Elaboration, and Coherence
  458. Theorem 21.8 — Decision of simple disjointnessDisjoint Intersections, Merge Elaboration, and Coherence
  459. Lemma 21.10 — Unique coercionsDisjoint Intersections, Merge Elaboration, and Coherence
  460. Lemma 21.11 — Unique synthesisDisjoint Intersections, Merge Elaboration, and Coherence
  461. Theorem 21.12 — Elaboration preserves typesDisjoint Intersections, Merge Elaboration, and Coherence
  462. Theorem 21.13 — Coherence of the frozen elaborationDisjoint Intersections, Merge Elaboration, and Coherence
  463. Corollary 21.14 — Safety and deterministic meaningDisjoint Intersections, Merge Elaboration, and Coherence
  464. Proposition 10.2 — The unguarded last index is stuckRefinement Types and Proof-Carrying Programs
  465. Lemma 22.8 — Semantic substitution for predicate verticesRefinement Types and Proof-Carrying Programs
  466. Lemma 10.7 — Path and negative-cycle soundnessRefinement Types and Proof-Carrying Programs
  467. Lemma 10.8 — Potentials from absence of negative cyclesRefinement Types and Proof-Carrying Programs
  468. Theorem 10.9 — Certificate checker soundness and completenessRefinement Types and Proof-Carrying Programs
  469. Corollary 10.10 — Certificate-producing decisionRefinement Types and Proof-Carrying Programs
  470. Lemma 22.16 — Shape preservation for refinement subtypingRefinement Types and Proof-Carrying Programs
  471. Lemma 10.12 — Context implication and narrowingRefinement Types and Proof-Carrying Programs
  472. Proposition 10.13 — Subtyping lawsRefinement Types and Proof-Carrying Programs
  473. Lemma 22.20 — Regularity of synthesisRefinement Types and Proof-Carrying Programs
  474. Lemma 22.21 — Substitution commutes with representatives and guardsRefinement Types and Proof-Carrying Programs
  475. Lemma 10.16 — Subtyping VCs are exactRefinement Types and Proof-Carrying Programs
  476. Lemma 22.24 — Generated-output exactnessRefinement Types and Proof-Carrying Programs
  477. Lemma 22.25 — Declarative generation completenessRefinement Types and Proof-Carrying Programs
  478. Theorem 10.17 — VC-producing checker correctnessRefinement Types and Proof-Carrying Programs
  479. Lemma 10.18 — Atom reflection and static substitutionRefinement Types and Proof-Carrying Programs
  480. Lemma 22.28 — Application transportRefinement Types and Proof-Carrying Programs
  481. Lemma 10.19 — Typing under a more precise contextRefinement Types and Proof-Carrying Programs
  482. Lemma 10.20 — Weakening, atom reflection, and substitutionRefinement Types and Proof-Carrying Programs
  483. Lemma 10.21 — Canonical forms through subsumptionRefinement Types and Proof-Carrying Programs
  484. Lemma 10.22 — Typing bind compositionRefinement Types and Proof-Carrying Programs
  485. Lemma 10.23 — Valid-guard dischargeRefinement Types and Proof-Carrying Programs
  486. Theorem 10.24 — PreservationRefinement Types and Proof-Carrying Programs
  487. Theorem 10.25 — Progress up to checked errorRefinement Types and Proof-Carrying Programs
  488. Corollary 10.26 — Array safety and refinement soundnessRefinement Types and Proof-Carrying Programs
  489. Theorem 10.28 — Finite-qualifier inferenceRefinement Types and Proof-Carrying Programs
  490. Theorem 10.30 — Bounds-contract insertion and certified removalRefinement Types and Proof-Carrying Programs
  491. Theorem 10.32 — Source PCC acceptanceRefinement Types and Proof-Carrying Programs
  492. Lemma 10.34 — Measure indistinguishabilityRefinement Types and Proof-Carrying Programs
  493. Proposition 10.35 — Erasure boundaryRefinement Types and Proof-Carrying Programs
  494. Lemma 23.2 — Consistency reflexivityGradual Typing and the Dynamic Boundary
  495. Lemma 23.3 — Consistency symmetryGradual Typing and the Dynamic Boundary
  496. Proposition 23.4 — Unique source typesGradual Typing and the Dynamic Boundary
  497. Proposition 23.9 — Insertion is total, unique, and typedGradual Typing and the Dynamic Boundary
  498. Lemma 23.11 — Target substitutionGradual Typing and the Dynamic Boundary
  499. Lemma 23.12 — Canonical formsGradual Typing and the Dynamic Boundary
  500. Lemma 23.13 — A cast on a value progressesGradual Typing and the Dynamic Boundary
  501. Theorem 23.14 — PreservationGradual Typing and the Dynamic Boundary
  502. Theorem 23.15 — Progress and determinismGradual Typing and the Dynamic Boundary
  503. Corollary 23.16 — Safety of elaborated programsGradual Typing and the Dynamic Boundary
  504. Proposition 23.18 — Decidability of polar safetyGradual Typing and the Dynamic Boundary
  505. Lemma 23.19 — Polar reflexivityGradual Typing and the Dynamic Boundary
  506. Lemma 23.20 — Grounding preserves polar safetyGradual Typing and the Dynamic Boundary
  507. Lemma 23.22 — One-step preservation of label safetyGradual Typing and the Dynamic Boundary
  508. Theorem 23.23 — Positive and negative blameGradual Typing and the Dynamic Boundary
  509. Corollary 23.24 — Ownership at a typed–dynamic boundaryGradual Typing and the Dynamic Boundary
  510. Proposition 23.27 — Precision factors through polar safetyGradual Typing and the Dynamic Boundary
  511. Lemma 23.28 — Matching and consistency lose information monotonicallyGradual Typing and the Dynamic Boundary
  512. Theorem 23.29 — Static gradual guaranteeGradual Typing and the Dynamic Boundary
  513. Proposition 23.31 — Regularity of target precisionGradual Typing and the Dynamic Boundary
  514. Lemma 23.32 — Target precision reflexivityGradual Typing and the Dynamic Boundary
  515. Lemma 23.33 — Insertion preserves precisionGradual Typing and the Dynamic Boundary
  516. Lemma 23.35 — Open related substitutionGradual Typing and the Dynamic Boundary
  517. Lemma 23.37 — Frame pluggingGradual Typing and the Dynamic Boundary
  518. Lemma 23.38 — Common precision fixes a cast's shapeGradual Typing and the Dynamic Boundary
  519. Lemma 23.39 — One-sided injection and ground-tag coherenceGradual Typing and the Dynamic Boundary
  520. Lemma 23.40 — Value catch-upGradual Typing and the Dynamic Boundary
  521. Lemma 23.42 — Application roots have a nonempty matchGradual Typing and the Dynamic Boundary
  522. Lemma 23.43 — One-step simulation with accounted stutteringGradual Typing and the Dynamic Boundary
  523. Corollary 23.44 — Finite simulationGradual Typing and the Dynamic Boundary
  524. Theorem 23.46 — Infinite simulationGradual Typing and the Dynamic Boundary
  525. Corollary 23.47 — Operational trichotomyGradual Typing and the Dynamic Boundary
  526. Theorem 23.48 — Dynamic gradual guaranteeGradual Typing and the Dynamic Boundary
  527. Proposition 23.50 — Casts execute the contract translationGradual Typing and the Dynamic Boundary
  528. Proposition 23.51 — A coercion optimization needs an observation theoremGradual Typing and the Dynamic Boundary
  529. Proposition 23.52 — Static fragments cross without run-time failureGradual Typing and the Dynamic Boundary
  530. Theorem 23.54 — Imported safety boundary for SDGradual Typing and the Dynamic Boundary
  531. Lemma 24.2 — Composition of distinct type substitutionsRecursive Types, Domains, and General Recursion
  532. Lemma 24.3 — Type and term substitutionRecursive Types, Domains, and General Recursion
  533. Lemma 24.4 — Folded canonical formsRecursive Types, Domains, and General Recursion
  534. Theorem 24.5 — Preservation, progress, and safetyRecursive Types, Domains, and General Recursion
  535. Theorem 24.8 — Decision of contractive regular equalityRecursive Types, Domains, and General Recursion
  536. Lemma 24.11 — Unique call-by-name decompositionRecursive Types, Domains, and General Recursion
  537. Lemma 24.12 — PCF structural and safety propertiesRecursive Types, Domains, and General Recursion
  538. Lemma 24.14 — Orders used by the recursive equationRecursive Types, Domains, and General Recursion
  539. Lemma 24.15 — Continuous function spacesRecursive Types, Domains, and General Recursion
  540. Lemma 24.16 — Continuous pairing, evaluation, and curryingRecursive Types, Domains, and General Recursion
  541. Theorem 24.17 — Kleene least fixed pointRecursive Types, Domains, and General Recursion
  542. Lemma 24.20 — Continuity of the least-fixed-point operatorRecursive Types, Domains, and General Recursion
  543. Lemma 24.21 — Parameterized least fixed pointsRecursive Types, Domains, and General Recursion
  544. Lemma 24.22 — Admissible fixed-point inductionRecursive Types, Domains, and General Recursion
  545. Lemma 24.24 — Finite observations determine the partial-list orderRecursive Types, Domains, and General Recursion
  546. Lemma 24.25 — The lazy-list omega-cpoRecursive Types, Domains, and General Recursion
  547. Lemma 24.26 — Compact lazy listsRecursive Types, Domains, and General Recursion
  548. Lemma 24.27 — The lazy-list unfolding isomorphismRecursive Types, Domains, and General Recursion
  549. Proposition 24.28 — The lazy list solutionRecursive Types, Domains, and General Recursion
  550. Proposition 24.29 — Finite operational lists commute with outRecursive Types, Domains, and General Recursion
  551. Lemma 24.31 — Continuity of the strict natural operationsRecursive Types, Domains, and General Recursion
  552. Lemma 24.33 — Semantic typing and continuityRecursive Types, Domains, and General Recursion
  553. Lemma 24.34 — Semantic substitution and reduction invarianceRecursive Types, Domains, and General Recursion
  554. Lemma 24.36 — Finite anti-reductionRecursive Types, Domains, and General Recursion
  555. Lemma 24.37 — Admissibility of logical approximationRecursive Types, Domains, and General Recursion
  556. Theorem 24.38 — Fundamental approximationRecursive Types, Domains, and General Recursion
  557. Theorem 24.39 — Computational adequacy for closed naturalsRecursive Types, Domains, and General Recursion
  558. Lemma 24.42 — Unique indexed decompositionRecursive Types, Domains, and General Recursion
  559. Lemma 24.43 — Terminating-trace decompositionRecursive Types, Domains, and General Recursion
  560. Lemma 24.44 — Indexed downward closure and anti-reductionRecursive Types, Domains, and General Recursion
  561. Lemma 24.45 — Indexed fundamental lemmaRecursive Types, Domains, and General Recursion
  562. Lemma 24.46 — Indexed evaluation-context compatibilityRecursive Types, Domains, and General Recursion
  563. Lemma 24.47 — Indexed structural packageRecursive Types, Domains, and General Recursion
  564. Proposition 24.49 — The eta-delayed equation is pointwiseRecursive Types, Domains, and General Recursion
  565. Lemma 24.50 — Structural convergence of the copierRecursive Types, Domains, and General Recursion
  566. Theorem 24.51 — Recursive list copyRecursive Types, Domains, and General Recursion
  567. Proposition 24.54 — The five notions separateRecursive Types, Domains, and General Recursion
  568. Theorem 24.56 — Unrestricted recursion is not a total proof principleRecursive Types, Domains, and General Recursion
  569. Lemma 15.3 — Structural properties of Ob_1Object Calculi and Recursive Object Types
  570. Lemma 15.4 — Object canonical formsObject Calculi and Recursive Object Types
  571. Theorem 15.5 — Safety of the functional object calculusObject Calculi and Recursive Object Types
  572. Lemma 25.8 — Top is maximal in object subtypingObject Calculi and Recursive Object Types
  573. Lemma 25.9 — Inversion of width-invariant object subtypingObject Calculi and Recursive Object Types
  574. Lemma 15.8 — Narrowing the receiverObject Calculi and Recursive Object Types
  575. Lemma 15.9 — Source substitution with subtypingObject Calculi and Recursive Object Types
  576. Theorem 15.10 — Minimum typingObject Calculi and Recursive Object Types
  577. Theorem 15.11 — Safety with width-invariant subtypingObject Calculi and Recursive Object Types
  578. Proposition 15.12 — Covariant method components destroy preservationObject Calculi and Recursive Object Types
  579. Lemma 15.14 — The two substitutionsObject Calculi and Recursive Object Types
  580. Proposition 15.15 — Safety of recursive objectsObject Calculi and Recursive Object Types
  581. Lemma 25.20 — Top is maximal in target subtypingObject Calculi and Recursive Object Types
  582. Lemma 15.18 — Target narrowing and substitutionObject Calculi and Recursive Object Types
  583. Lemma 25.23 — Existential inversion and the generalized open rootObject Calculi and Recursive Object Types
  584. Lemma 15.19 — Width is preserved by the type translationObject Calculi and Recursive Object Types
  585. Lemma 15.20 — The visible-method target boundObject Calculi and Recursive Object Types
  586. Lemma 25.26 — Translation is invariant under receiver narrowingObject Calculi and Recursive Object Types
  587. Lemma 15.21 — Translation commutes with source substitutionObject Calculi and Recursive Object Types
  588. Theorem 25.28 — Scoped typing of the object translationObject Calculi and Recursive Object Types
  589. Theorem 15.22 — Scoped typing and simulationObject Calculi and Recursive Object Types
  590. Lemma 26.2 — Constraint characterizationCorrected Inference for Simple Objects
  591. Lemma 26.3 — Four-way overwrite decompositionCorrected Inference for Simple Objects
  592. Lemma 26.5 — Shared-variable equivalenceCorrected Inference for Simple Objects
  593. Lemma 26.6 — Termination measure for the corrected row phaseCorrected Inference for Simple Objects
  594. Proposition 26.7 — No principal scheme for WCorrected Inference for Simple Objects
  595. Theorem 26.8 — Corrigendum boundary: finite complete setsCorrected Inference for Simple Objects
  596. Lemma 26.9 — Concatenation constraints are exactCorrected Inference for Simple Objects
  597. Theorem 26.10 — Finite complete sets for record concatenationCorrected Inference for Simple Objects
  598. Lemma 16.3 — Polarity is monotonicityOO Self Types, F-Bounds, and Matching
  599. Lemma 16.6 — Structural properties of Self_+OO Self Types, F-Bounds, and Matching
  600. Lemma 27.6 — Outer-shape inversionOO Self Types, F-Bounds, and Matching
  601. Lemma 16.7 — Self-subtyping inversionOO Self Types, F-Bounds, and Matching
  602. Lemma 16.8 — Canonical formsOO Self Types, F-Bounds, and Matching
  603. Theorem 16.9 — PreservationOO Self Types, F-Bounds, and Matching
  604. Theorem 16.10 — Progress and functional safetyOO Self Types, F-Bounds, and Matching
  605. Lemma 16.12 — F-bound instantiationOO Self Types, F-Bounds, and Matching
  606. Proposition 21.12 — Boundary of the public-witness comparisonOO Self Types, F-Bounds, and Matching
  607. Proposition 16.14 — Reflexivity and transitivity of matchingOO Self Types, F-Bounds, and Matching
  608. Theorem 16.15 — Soundness of the operator readingOO Self Types, F-Bounds, and Matching
  609. Lemma 27.19 — Store-typing weakeningOO Self Types, F-Bounds, and Matching
  610. Theorem 21.17 — Configuration preservationOO Self Types, F-Bounds, and Matching
  611. Theorem 21.18 — Configuration progressOO Self Types, F-Bounds, and Matching
  612. Corollary 21.19 — Syntactic state safetyOO Self Types, F-Bounds, and Matching
  613. Lemma 21.22 — Closing substitution and semantic subtypingOO Self Types, F-Bounds, and Matching
  614. Lemma 27.26 — Expression anti-reductionOO Self Types, F-Bounds, and Matching
  615. Lemma 27.27 — Compatibility of the reference formsOO Self Types, F-Bounds, and Matching
  616. Theorem 21.23 — Fundamental theorem for the imperative Self fragmentOO Self Types, F-Bounds, and Matching
  617. Corollary 21.24 — Semantic state safetyOO Self Types, F-Bounds, and Matching
  618. Lemma 22.4 — Monad laws forced by sequencingEffects, Monads, CBPV, and Algebraic Operations
  619. Proposition 22.5 — Algebraicity of a requested operationEffects, Monads, CBPV, and Algebraic Operations
  620. Theorem 22.8 — Existence and uniqueness of handlingEffects, Monads, CBPV, and Algebraic Operations
  621. Lemma 28.9 — Fold after tree sequencingEffects, Monads, CBPV, and Algebraic Operations
  622. Corollary 22.9 — Quotient descentEffects, Monads, CBPV, and Algebraic Operations
  623. Lemma 22.12 — Structural lemmas for CBPV_0Effects, Monads, CBPV, and Algebraic Operations
  624. Lemma 22.13 — Canonical terminal computationsEffects, Monads, CBPV, and Algebraic Operations
  625. Theorem 22.14 — Safety of CBPV_0Effects, Monads, CBPV, and Algebraic Operations
  626. Lemma 22.15 — Typing of both translationsEffects, Monads, CBPV, and Algebraic Operations
  627. Lemma 22.16 — Translation and substitutionEffects, Monads, CBPV, and Algebraic Operations
  628. Lemma 28.18 — Administrative normal forms and substitutionEffects, Monads, CBPV, and Algebraic Operations
  629. Lemma 28.19 — Weak steps across administrative normalizationEffects, Monads, CBPV, and Algebraic Operations
  630. Lemma 22.17 — Administrative transport for weak CBPV evaluationEffects, Monads, CBPV, and Algebraic Operations
  631. Lemma 22.18 — Translated trace decompositionEffects, Monads, CBPV, and Algebraic Operations
  632. Theorem 22.19 — Evaluation-order simulationsEffects, Monads, CBPV, and Algebraic Operations
  633. Lemma 28.25 — Soundness and completeness of handler constraintsEffects, Monads, CBPV, and Algebraic Operations
  634. Lemma 28.26 — Boundary normalization of effect weakeningEffects, Monads, CBPV, and Algebraic Operations
  635. Proposition 22.22 — Least synthesized effectEffects, Monads, CBPV, and Algebraic Operations
  636. Lemma 22.23 — Substitution and replacementEffects, Monads, CBPV, and Algebraic Operations
  637. Lemma 22.24 — Typed operation decompositionEffects, Monads, CBPV, and Algebraic Operations
  638. Theorem 22.25 — PreservationEffects, Monads, CBPV, and Algebraic Operations
  639. Theorem 22.26 — Progress up to an exposed operationEffects, Monads, CBPV, and Algebraic Operations
  640. Corollary 22.27 — Fully handled safetyEffects, Monads, CBPV, and Algebraic Operations
  641. Lemma 22.29 — Reification through an open contextEffects, Monads, CBPV, and Algebraic Operations
  642. Lemma 22.30 — Administrative reification of a deep continuationEffects, Monads, CBPV, and Algebraic Operations
  643. Theorem 22.31 — Handler/tree agreementEffects, Monads, CBPV, and Algebraic Operations
  644. Proposition 23.3 — Existence for the finitely branching running signaturesScoped Operations and Explicit Substitution
  645. Lemma 23.5 — Canonical nested representativeScoped Operations and Explicit Substitution
  646. Lemma 23.6 — Well-founded elementwise recursionScoped Operations and Explicit Substitution
  647. Corollary 23.7 — Elementwise inductionScoped Operations and Explicit Substitution
  648. Lemma 23.10 — Substitution respects reindexingScoped Operations and Explicit Substitution
  649. Theorem 23.11 — Explicit-substitution equationsScoped Operations and Explicit Substitution
  650. Corollary 23.12 — Scoped-syntax monadScoped Operations and Explicit Substitution
  651. Lemma 23.13 — Renaming is return substitutionScoped Operations and Explicit Substitution
  652. Proposition 23.15 — Monad-induced idiomScoped Operations and Explicit Substitution
  653. Proposition 23.16 — Kleisli category and product actionScoped Operations and Explicit Substitution
  654. Proposition 23.18 — Continuation-adapter criterionScoped Operations and Explicit Substitution
  655. Proposition 24.1 — First-order fold obstructionHigher-Order Algebraic Effects and Modular Elaboration
  656. Theorem 24.8 — Monad equations for hefty bindHigher-Order Algebraic Effects and Modular Elaboration
  657. Lemma 24.11 — Unique structural solutionHigher-Order Algebraic Effects and Modular Elaboration
  658. Theorem 24.13 — Typing by constructionHigher-Order Algebraic Effects and Modular Elaboration
  659. Proposition 24.15 — Canonical insertion on duplicate-free rowsHigher-Order Algebraic Effects and Modular Elaboration
  660. Proposition 24.19 — Typing of the catch clauseHigher-Order Algebraic Effects and Modular Elaboration
  661. Theorem 24.23 — Modular elaboration equationsHigher-Order Algebraic Effects and Modular Elaboration
  662. Proposition 24.24 — Composition coherence under reassociationHigher-Order Algebraic Effects and Modular Elaboration
  663. Proposition 24.26 — Global-state transaction calculationHigher-Order Algebraic Effects and Modular Elaboration
  664. Lemma 24.27 — Throw handling distributes through bindHigher-Order Algebraic Effects and Modular Elaboration
  665. Lemma 24.28 — Handling a masked treeHigher-Order Algebraic Effects and Modular Elaboration
  666. Proposition 24.29 — Observable catch equationHigher-Order Algebraic Effects and Modular Elaboration
  667. Theorem 24.30 — Lawfulness equations for modular catchHigher-Order Algebraic Effects and Modular Elaboration
  668. Lemma 25.2 — CancellationEffect Rows, Principal Type-and-Effect Inference, and Handlers
  669. Lemma 25.6 — Nearest-handler decompositionEffect Rows, Principal Type-and-Effect Inference, and Handlers
  670. Lemma 25.7 — Replacement for request contextsEffect Rows, Principal Type-and-Effect Inference, and Handlers
  671. Lemma 31.8 — Type-and-row action and scheme enlargementEffect Rows, Principal Type-and-Effect Inference, and Handlers
  672. Lemma 25.8 — Type, row, ordinary, and generalized substitutionEffect Rows, Principal Type-and-Effect Inference, and Handlers
  673. Lemma 31.10 — Generalized value substitutionEffect Rows, Principal Type-and-Effect Inference, and Handlers
  674. Lemma 31.11 — Arrow canonical formEffect Rows, Principal Type-and-Effect Inference, and Handlers
  675. Theorem 25.9 — PreservationEffect Rows, Principal Type-and-Effect Inference, and Handlers
  676. Theorem 25.10 — Progress and absence of unhandled operationsEffect Rows, Principal Type-and-Effect Inference, and Handlers
  677. Lemma 25.12 — ExposureEffect Rows, Principal Type-and-Effect Inference, and Handlers
  678. Lemma 25.13 — TerminationEffect Rows, Principal Type-and-Effect Inference, and Handlers
  679. Theorem 25.14 — Most-general type-and-row unificationEffect Rows, Principal Type-and-Effect Inference, and Handlers
  680. Lemma 25.16 — Computation and pure-let generalizationEffect Rows, Principal Type-and-Effect Inference, and Handlers
  681. Theorem 25.17 — Soundness of inferenceEffect Rows, Principal Type-and-Effect Inference, and Handlers
  682. Lemma 31.21 — Non-handler factorization stepEffect Rows, Principal Type-and-Effect Inference, and Handlers
  683. Lemma 31.22 — Handler-accumulator factorization stepEffect Rows, Principal Type-and-Effect Inference, and Handlers
  684. Theorem 25.18 — Completeness and principal factorizationEffect Rows, Principal Type-and-Effect Inference, and Handlers
  685. Theorem 25.19 — Closed-row support translationEffect Rows, Principal Type-and-Effect Inference, and Handlers
  686. Theorem 31.26 — Internal-safe preservationEffect Rows, Principal Type-and-Effect Inference, and Handlers
  687. Theorem 31.27 — Internal-safe progressEffect Rows, Principal Type-and-Effect Inference, and Handlers
  688. Theorem 31.28 — Live-marker uniquenessEffect Rows, Principal Type-and-Effect Inference, and Handlers
  689. Theorem 31.29 — Generalized-evidence operational endpointEffect Rows, Principal Type-and-Effect Inference, and Handlers
  690. Theorem 31.30 — Effect exclusion safetyEffect Rows, Principal Type-and-Effect Inference, and Handlers
  691. Theorem 31.31 — Effect-exclusion machine safetyEffect Rows, Principal Type-and-Effect Inference, and Handlers
  692. Lemma 32.4 — Generatedness closureEffect Capabilities and Tunnelling
  693. Lemma 32.5 — Ordered insertion weakeningEffect Capabilities and Tunnelling
  694. Lemma 32.6 — Block-context exchange and identical shadowingEffect Capabilities and Tunnelling
  695. Lemma 32.7 — Value and scope-respecting block substitutionEffect Capabilities and Tunnelling
  696. Lemma 32.8 — Canonical formsEffect Capabilities and Tunnelling
  697. Lemma 32.9 — Label-aware progressEffect Capabilities and Tunnelling
  698. Theorem 32.10 — Progress for System XiEffect Capabilities and Tunnelling
  699. Lemma 32.11 — Typed evaluation-context replacementEffect Capabilities and Tunnelling
  700. Theorem 32.12 — PreservationEffect Capabilities and Tunnelling
  701. Corollary 32.13 — System Xi label safetyEffect Capabilities and Tunnelling
  702. Theorem 32.15 — Effekt-to-System- Xi type preservationEffect Capabilities and Tunnelling
  703. Corollary 32.16 — Effekt effect safetyEffect Capabilities and Tunnelling
  704. Lemma 32.19 — Delimiter compatibilityEffect Capabilities and Tunnelling
  705. Lemma 32.20 — Handler-definition compatibilityEffect Capabilities and Tunnelling
  706. Lemma 32.21 — Compatibility mechanismEffect Capabilities and Tunnelling
  707. Lemma 32.23 — AdequacyEffect Capabilities and Tunnelling
  708. Corollary 32.24 — Tunnelling parametricityEffect Capabilities and Tunnelling
  709. Theorem 32.25 — Tunnelling metatheoremsEffect Capabilities and Tunnelling
  710. Theorem 32.26 — Olaf source metatheoremsEffect Capabilities and Tunnelling
  711. Theorem 33.2 — Met safetyModal Effect Types and Source-to-Met Encodings
  712. Theorem 33.3 — Row-to-Met preservationModal Effect Types and Source-to-Met Encodings
  713. Theorem 33.4 — Capability-to-Met preservationModal Effect Types and Source-to-Met Encodings
  714. Proposition 34.6 — The exchanger invariantLexical Effect Handlers and Direct Compilation
  715. Lemma 34.7 — Positive simulation criterionLexical Effect Handlers and Direct Compilation
  716. Theorem 34.8 — Lexa-to-Salt semantic preservationLexical Effect Handlers and Direct Compilation
  717. Theorem 34.11 — SL-to-TL simulation and terminating preservationLexical Effect Handlers and Direct Compilation
  718. Proposition 34.12 — The exact zero-mainline propertyLexical Effect Handlers and Direct Compilation
  719. Theorem 34.14 — The generalised-continuation endpointsLexical Effect Handlers and Direct Compilation
  720. Lemma 35.2 — Closed value substitution and canonical continuationsControl Operators and Classical Proofs
  721. Theorem 35.3 — Machine preservationControl Operators and Classical Proofs
  722. Theorem 35.4 — Machine progressControl Operators and Classical Proofs
  723. Corollary 35.5 — SafetyControl Operators and Classical Proofs
  724. Proposition 35.6 — Normalization of the CPS targetControl Operators and Classical Proofs
  725. Lemma 35.10 — CPS substitutionControl Operators and Classical Proofs
  726. Theorem 35.11 — CPS type preservationControl Operators and Classical Proofs
  727. Theorem 35.12 — Positive-step machine simulationControl Operators and Classical Proofs
  728. Theorem 35.13 — Termination of the λ _ K machineControl Operators and Classical Proofs
  729. Corollary 35.14 — Relative consistency of the continuation calculusControl Operators and Classical Proofs
  730. Proposition 35.15 — Continuation-form double negationControl Operators and Classical Proofs
  731. Proposition 35.16 — Continuation-form excluded middle with a change-of-mind traceControl Operators and Classical Proofs
  732. Corollary 35.17 — Double-negation elimination and excluded middleControl Operators and Classical Proofs
  733. Lemma 35.22 — Deep-bridge type substitutionControl Operators and Classical Proofs
  734. Lemma 35.23 — Deep-bridge value substitutionControl Operators and Classical Proofs
  735. Lemma 35.24 — Deep-bridge context compatibilityControl Operators and Classical Proofs
  736. Lemma 35.25 — Deep-bridge translation algebraControl Operators and Classical Proofs
  737. Lemma 35.26 — Deep-bridge formationControl Operators and Classical Proofs
  738. Lemma 35.27 — shift_0-to-deep type preservationControl Operators and Classical Proofs
  739. Lemma 35.28 — Deep-to- shift_0 type preservationControl Operators and Classical Proofs
  740. Lemma 35.29 — Deep-bridge root simulationControl Operators and Classical Proofs
  741. Theorem 35.30 — Typed deep/ shift_0 correspondenceControl Operators and Classical Proofs
  742. Lemma 35.33 — Shallow-bridge type substitutionControl Operators and Classical Proofs
  743. Lemma 35.34 — Shallow-bridge value substitutionControl Operators and Classical Proofs
  744. Lemma 35.35 — Shallow-bridge context compatibilityControl Operators and Classical Proofs
  745. Lemma 35.36 — Shallow-bridge translation algebraControl Operators and Classical Proofs
  746. Lemma 35.37 — Forward shallow-bridge preservationControl Operators and Classical Proofs
  747. Lemma 35.38 — Reverse shallow-bridge preservationControl Operators and Classical Proofs
  748. Lemma 35.39 — Shallow-bridge root simulationControl Operators and Classical Proofs
  749. Theorem 35.40 — Typed shallow/ control_0 correspondenceControl Operators and Classical Proofs
  750. Proposition 35.42 — The dependent-elimination boundaryControl Operators and Classical Proofs
  751. Lemma 35.44 — Admissible type substitutionControl Operators and Classical Proofs
  752. Lemma 35.45 — Generalized Damas–Milner substitutionControl Operators and Classical Proofs
  753. Theorem 35.46 — Values-only soundnessControl Operators and Classical Proofs
  754. Lemma 18.2 — Split algebraLinear and Affine Type Systems
  755. Proposition 18.8 — The read-close derivationLinear and Affine Type Systems
  756. Lemma 18.9 — Exchange and unrestricted weakeningLinear and Affine Type Systems
  757. Lemma 18.10 — Unrestricted substitutionLinear and Affine Type Systems
  758. Lemma 18.11 — Linear substitutionLinear and Affine Type Systems
  759. Corollary 18.12 — Two-variable linear substitutionLinear and Affine Type Systems
  760. Theorem 18.14 — Exact pathwise useLinear and Affine Type Systems
  761. Lemma 18.15 — Canonical formsLinear and Affine Type Systems
  762. Lemma 18.16 — Evaluation-context replacementLinear and Affine Type Systems
  763. Theorem 18.17 — PreservationLinear and Affine Type Systems
  764. Theorem 18.18 — Progress and ordinary safetyLinear and Affine Type Systems
  765. Lemma 36.21 — Fresh-token insertionLinear and Affine Type Systems
  766. Lemma 36.22 — Active token factorizationLinear and Affine Type Systems
  767. Theorem 18.20 — File-token preservation and cleanupLinear and Affine Type Systems
  768. Proposition 18.21 — Principal cut computationsLinear and Affine Type Systems
  769. Proposition 18.22 — One commuting cutLinear and Affine Type Systems
  770. Lemma 36.27 — Simultaneous substitutionLinear and Affine Type Systems
  771. Lemma 36.28 — Substitution in every structural regimeLinear and Affine Type Systems
  772. Lemma 36.29 — Reduction reflects variable identificationLinear and Affine Type Systems
  773. Theorem 36.30 — Safety after each structural deltaLinear and Affine Type Systems
  774. Proposition 36.31 — The file boundary in the four regimesLinear and Affine Type Systems
  775. Proposition 36.33 — Four different notions at zeroLinear and Affine Type Systems
  776. Lemma 37.3 — Target substitutionEvaluation-Strategy Translations
  777. Theorem 37.4 — Subject reduction for the linear targetEvaluation-Strategy Translations
  778. Lemma 37.5 — Name substitution and typingEvaluation-Strategy Translations
  779. Theorem 37.6 — Exact call-by-name translationEvaluation-Strategy Translations
  780. Lemma 37.8 — Conservative administrative completionEvaluation-Strategy Translations
  781. Theorem 37.9 — Exact call-by-value translationEvaluation-Strategy Translations
  782. Corollary 37.11 — Affine target subject reductionEvaluation-Strategy Translations
  783. Theorem 37.12 — Exact call-by-need translationEvaluation-Strategy Translations
  784. Proposition 37.13 — Opening obstructionEvaluation-Strategy Translations
  785. Lemma 38.3 — Atomic last ruleOrdered and Noncommutative Types and the Lambek Calculus
  786. Proposition 38.4 — Illegal exchangeOrdered and Noncommutative Types and the Lambek Calculus
  787. Theorem 38.6 — Ordered single-cut admissibilityOrdered and Noncommutative Types and the Lambek Calculus
  788. Corollary 38.7 — Ordered simultaneous substitutionOrdered and Noncommutative Types and the Lambek Calculus
  789. Theorem 38.8 — Cut eliminationOrdered and Noncommutative Types and the Lambek Calculus
  790. Theorem 38.9 — ResiduationOrdered and Noncommutative Types and the Lambek Calculus
  791. Lemma 38.12 — Strict descentOrdered and Noncommutative Types and the Lambek Calculus
  792. Theorem 38.13 — Decidability and exactness of searchOrdered and Noncommutative Types and the Lambek Calculus
  793. Proposition 38.14 — A visible word-order failureOrdered and Noncommutative Types and the Lambek Calculus
  794. Proposition 38.16 — The exact structural boundaryOrdered and Noncommutative Types and the Lambek Calculus
  795. Proposition 38.17 — Exchange identifies the two residualsOrdered and Noncommutative Types and the Lambek Calculus
  796. Lemma 39.2 — Invertibility of the ordinary inversion rulesPolarization, Focusing, and Proof Search
  797. Lemma 39.9 — Heredity of suspension normalityPolarization, Focusing, and Proof Search
  798. Lemma 39.10 — Focused persistent structural rulesPolarization, Focusing, and Proof Search
  799. Lemma 39.12 — Queued positive-left rulesPolarization, Focusing, and Proof Search
  800. Theorem 39.13 — De-focalizationPolarization, Focusing, and Proof Search
  801. Lemma 39.14 — Focal substitutionPolarization, Focusing, and Proof Search
  802. Theorem 39.15 — Focused cut admissibilityPolarization, Focusing, and Proof Search
  803. Theorem 39.16 — Identity expansionPolarization, Focusing, and Proof Search
  804. Lemma 39.17 — Removal of adjacent shiftsPolarization, Focusing, and Proof Search
  805. Lemma 39.18 — Unfocused rules are admissible under polarizationPolarization, Focusing, and Proof Search
  806. Theorem 39.19 — FocalizationPolarization, Focusing, and Proof Search
  807. Corollary 39.20 — Ordinary cut, subformulas, and consistencyPolarization, Focusing, and Proof Search
  808. Lemma 39.22 — Finite, rule-closed candidate spacePolarization, Focusing, and Proof Search
  809. Theorem 39.23 — Decision procedure for focused provabilityPolarization, Focusing, and Proof Search
  810. Corollary 39.24 — Terminating goal-directed searchPolarization, Focusing, and Proof Search
  811. Lemma 40.2 — Expanded identityProof Nets, Correctness Criteria, and Cut Elimination
  812. Lemma 40.8 — Rule preservationProof Nets, Correctness Criteria, and Cut Elimination
  813. Theorem 40.9 — Soundness of the switching criterionProof Nets, Correctness Criteria, and Cut Elimination
  814. Lemma 40.11 — Subnet algebraProof Nets, Correctness Criteria, and Cut Elimination
  815. Lemma 40.12 — Crossing an empire boundaryProof Nets, Correctness Criteria, and Cut Elimination
  816. Lemma 40.13 — Kingdom of a tensorProof Nets, Correctness Criteria, and Cut Elimination
  817. Lemma 40.14 — Kingdom nestingProof Nets, Correctness Criteria, and Cut Elimination
  818. Lemma 40.15 — Kingdom orderProof Nets, Correctness Criteria, and Cut Elimination
  819. Lemma 40.16 — Splitting tensorProof Nets, Correctness Criteria, and Cut Elimination
  820. Theorem 40.17 — SequentializationProof Nets, Correctness Criteria, and Cut Elimination
  821. Proposition 40.19 — Correctness and complexity of the direct checkerProof Nets, Correctness Criteria, and Cut Elimination
  822. Theorem 40.20 — Linear correctness checkingProof Nets, Correctness Criteria, and Cut Elimination
  823. Lemma 40.23 — Correctness is preservedProof Nets, Correctness Criteria, and Cut Elimination
  824. Lemma 40.24 — TerminationProof Nets, Correctness Criteria, and Cut Elimination
  825. Corollary 40.25 — Cut-step boundProof Nets, Correctness Criteria, and Cut Elimination
  826. Lemma 40.26 — Local confluenceProof Nets, Correctness Criteria, and Cut Elimination
  827. Lemma 40.27 — Newman's lemmaProof Nets, Correctness Criteria, and Cut Elimination
  828. Theorem 40.28 — Cut normalization and confluenceProof Nets, Correctness Criteria, and Cut Elimination
  829. Corollary 40.29 — Sequent cut eliminationProof Nets, Correctness Criteria, and Cut Elimination
  830. Corollary 40.30 — Subformula property and a nonprovability consequenceProof Nets, Correctness Criteria, and Cut Elimination
  831. Lemma 40.32 — Phase orderingProof Nets, Correctness Criteria, and Cut Elimination
  832. Lemma 40.33 — Terminal-rule permutationProof Nets, Correctness Criteria, and Cut Elimination
  833. Theorem 40.34 — Proof nets as a quotient of proofsProof Nets, Correctness Criteria, and Cut Elimination
  834. Lemma 41.5 — Distinct redexes are disjointInteraction Nets and Interaction Combinators
  835. Proposition 41.7 — Addition calculatesInteraction Nets and Interaction Combinators
  836. Theorem 41.9 — Strong confluence of interaction systemsInteraction Nets and Interaction Combinators
  837. Corollary 41.10 — ConfluenceInteraction Nets and Interaction Combinators
  838. Theorem 41.12 — Independence of developmentsInteraction Nets and Interaction Combinators
  839. Theorem 41.14 — One beta stepInteraction Nets and Interaction Combinators
  840. Corollary 41.15 — Exact beta correspondenceInteraction Nets and Interaction Combinators
  841. Proposition 41.16 — Resource-manager calculationInteraction Nets and Interaction Combinators
  842. Theorem 41.17 — Finite nonlinear beta simulation and reflectionInteraction Nets and Interaction Combinators
  843. Theorem 41.18 — Universality of interaction combinatorsInteraction Nets and Interaction Combinators
  844. Proposition 41.19 — The deterministic hypothesis is necessaryInteraction Nets and Interaction Combinators
  845. Theorem 41.20 — Typed INMPP safety, reconstructedInteraction Nets and Interaction Combinators
  846. Theorem 41.21 — INMPP–INAMB operational correspondence, importedInteraction Nets and Interaction Combinators
  847. Proposition 41.22 — Queue invariantInteraction Nets and Interaction Combinators
  848. Proposition 42.2 — One graph contraction discharges both residualsOptimal Sharing and Graph Reduction
  849. Theorem 42.6 — Readback and family nonduplication, importedOptimal Sharing and Graph Reduction
  850. Proposition 42.8 — Prerequisite package for the cost obstructionOptimal Sharing and Graph Reduction
  851. Theorem 42.9 — Parallel-beta cost obstruction, importedOptimal Sharing and Graph Reduction
  852. Corollary 42.10 — Transfer to Lamping graph reduction, importedOptimal Sharing and Graph Reduction
  853. Corollary 42.11 — Ordinary versus parallel beta, importedOptimal Sharing and Graph Reduction
  854. Proposition 43.4 — Structural-congruence invarianceBunched Implications and Resource Semantics
  855. Proposition 43.6 — Scope of additive weakening and contractionBunched Implications and Resource Semantics
  856. Theorem 43.8 — Identity expansionBunched Implications and Resource Semantics
  857. Theorem 43.10 — Displayed multicut admissibilityBunched Implications and Resource Semantics
  858. Corollary 43.11 — Displayed substitution and cutBunched Implications and Resource Semantics
  859. Theorem 43.13 — Cut eliminationBunched Implications and Resource Semantics
  860. Lemma 43.15 — Cut-free invertibility, importedBunched Implications and Resource Semantics
  861. Lemma 43.17 — Structural closure propertiesBunched Implications and Resource Semantics
  862. Lemma 43.18 — The two residuals are closedBunched Implications and Resource Semantics
  863. Proposition 43.20 — Closed sets form a BI algebraBunched Implications and Resource Semantics
  864. Lemma 43.21 — Okada propertyBunched Implications and Resource Semantics
  865. Theorem 43.22 — Universal-algebra reflectionBunched Implications and Resource Semantics
  866. Theorem 43.23 — Algebraic soundness, importedBunched Implications and Resource Semantics
  867. Corollary 43.24 — Semantic cut certificateBunched Implications and Resource Semantics
  868. Lemma 43.27 — PersistenceBunched Implications and Resource Semantics
  869. Lemma 43.29 — Monotonicity of bunch contextsBunched Implications and Resource Semantics
  870. Proposition 43.30 — Weakening, contraction, and interchange failBunched Implications and Resource Semantics
  871. Theorem 43.31 — Soundness of LBI_0Bunched Implications and Resource Semantics
  872. Corollary 43.32 — Forbidden multiplicative structure is not admissibleBunched Implications and Resource Semantics
  873. Corollary 43.33 — Atomic non-derivabilityBunched Implications and Resource Semantics
  874. Lemma 43.34 — A bunch and its represented formulaBunched Implications and Resource Semantics
  875. Lemma 43.36 — The term frame is well definedBunched Implications and Resource Semantics
  876. Theorem 43.37 — Term-model truth lemmaBunched Implications and Resource Semantics
  877. Corollary 43.38 — Elementary completeness without disjunctionBunched Implications and Resource Semantics
  878. Lemma 43.39 — Bridge to the source NBI presentationBunched Implications and Resource Semantics
  879. Lemma 43.40 — Order-dual presentationBunched Implications and Resource Semantics
  880. Lemma 44.2 — Finite-heap algebraSeparation Logic and Local Reasoning
  881. Proposition 44.4 — Separating algebraSeparation Logic and Local Reasoning
  882. Proposition 44.5 — The separating adjunctionSeparation Logic and Local Reasoning
  883. Lemma 44.8 — Commands change only modified variablesSeparation Logic and Local Reasoning
  884. Lemma 44.9 — Fresh-variable coincidenceSeparation Logic and Local Reasoning
  885. Theorem 44.11 — Locality of the command languageSeparation Logic and Local Reasoning
  886. Theorem 44.13 — Frame ruleSeparation Logic and Local Reasoning
  887. Lemma 44.14 — Assertion substitutionSeparation Logic and Local Reasoning
  888. Theorem 44.16 — Soundness of local Hoare reasoningSeparation Logic and Local Reasoning
  889. Proposition 44.17 — Swapping two disjoint cellsSeparation Logic and Local Reasoning
  890. Lemma 44.19 — Exact chain footprintSeparation Logic and Local Reasoning
  891. Proposition 44.20 — Prepending a cellSeparation Logic and Local Reasoning
  892. Proposition 44.21 — Removing the headSeparation Logic and Local Reasoning
  893. Proposition 44.22 — The exact guaranteeSeparation Logic and Local Reasoning
  894. Proposition 45.1 — Disjoint parallel ownership is insufficientConcurrent Separation Logic and Higher-Order Ghost State
  895. Proposition 45.5 — Fragment lower bound and successful updateConcurrent Separation Logic and Higher-Order Ghost State
  896. Proposition 45.7 — Saved-proposition agreementConcurrent Separation Logic and Higher-Order Ghost State
  897. Theorem 45.9 — The physical increment is logically atomicConcurrent Separation Logic and Higher-Order Ghost State
  898. Theorem 45.10 — Concrete two-call client safetyConcurrent Separation Logic and Higher-Order Ghost State
  899. Corollary 45.11 — Adequacy boundaryConcurrent Separation Logic and Higher-Order Ghost State
  900. Proposition 45.12 — No independent deterministic exchanger stepsConcurrent Separation Logic and Higher-Order Ghost State
  901. Lemma 46.4 — One-command preservationOwnership, Borrowing, and Affine Resource Protocols
  902. Theorem 46.5 — Protocol progress and preservationOwnership, Borrowing, and Affine Resource Protocols
  903. Corollary 46.6 — No use after move and no dangling final borrowOwnership, Borrowing, and Affine Resource Protocols
  904. Proposition 46.7 — Protocol-step simulationOwnership, Borrowing, and Affine Resource Protocols
  905. Theorem 46.9 — Affe type soundness, importedOwnership, Borrowing, and Affine Resource Protocols
  906. Theorem 46.11 — Simplified uniqueness metatheory, importedOwnership, Borrowing, and Affine Resource Protocols
  907. Theorem 46.14 — Published Pure Borrow resultsOwnership, Borrowing, and Affine Resource Protocols
  908. Proposition 47.4 — Term–graph soundness and completenessUniqueness Types and Destructive Update
  909. Theorem 47.5 — Conventional subject reductionUniqueness Types and Destructive Update
  910. Lemma 47.7 — Exact equation generationUniqueness Types and Destructive Update
  911. Theorem 47.8 — Principal conventional typingUniqueness Types and Destructive Update
  912. Lemma 47.11 — Contraction matches graph sharingUniqueness Types and Destructive Update
  913. Theorem 47.12 — Uniqueness soundness and graph completenessUniqueness Types and Destructive Update
  914. Theorem 47.13 — Uniqueness subject reductionUniqueness Types and Destructive Update
  915. Lemma 47.15 — Effective closureUniqueness Types and Destructive Update
  916. Theorem 47.16 — Principal attribution, relative to a conventional solutionUniqueness Types and Destructive Update
  917. Proposition 47.17 — No claimed global principal uniqueness typeUniqueness Types and Destructive Update
  918. Theorem 47.19 — Eligible overwrite preserves the typed graph interfaceUniqueness Types and Destructive Update
  919. Lemma 48.4 — Projection-local invalidationPlace Calculi, Partial Moves, and Field-Sensitive Borrowing
  920. Lemma 48.5 — Borrow invariancePlace Calculi, Partial Moves, and Field-Sensitive Borrowing
  921. Theorem 48.6 — Featherweight Rust progressPlace Calculi, Partial Moves, and Field-Sensitive Borrowing
  922. Theorem 48.7 — Whole-term Featherweight Rust preservationPlace Calculi, Partial Moves, and Field-Sensitive Borrowing
  923. Theorem 48.8 — Featherweight Rust type and borrow safetyPlace Calculi, Partial Moves, and Field-Sensitive Borrowing
  924. Proposition 48.11 — Well-founded lookup measurePlace Calculi, Partial Moves, and Field-Sensitive Borrowing
  925. Theorem 48.12 — Termination of recursive place operationsPlace Calculi, Partial Moves, and Field-Sensitive Borrowing
  926. Lemma 48.13 — Linearizability is preservedPlace Calculi, Partial Moves, and Field-Sensitive Borrowing
  927. Corollary 48.14 — Borrow checking terminatesPlace Calculi, Partial Moves, and Field-Sensitive Borrowing
  928. Proposition 48.17 — Non-lexical releasePlace Calculi, Partial Moves, and Field-Sensitive Borrowing
  929. Lemma 48.18 — Stack-pop alignmentPlace Calculi, Partial Moves, and Field-Sensitive Borrowing
  930. Theorem 48.19 — Oxide v4 progressPlace Calculi, Partial Moves, and Field-Sensitive Borrowing
  931. Theorem 48.20 — Oxide v4 preservationPlace Calculi, Partial Moves, and Field-Sensitive Borrowing
  932. Corollary 48.21 — Oxide v4 type safetyPlace Calculi, Partial Moves, and Field-Sensitive Borrowing
  933. Lemma 49.2 — Unique descentMutable Value Semantics and inout Access
  934. Proposition 49.3 — Copy produces an independent valueMutable Value Semantics and inout Access
  935. Lemma 49.6 — Static separation implies physical disjointnessMutable Value Semantics and inout Access
  936. Theorem 49.9 — Safety of the conservative Swiftlet variantMutable Value Semantics and inout Access
  937. Corollary 49.10 — Static guaranteeMutable Value Semantics and inout Access
  938. Theorem 49.11 — Representation correspondence, source sketchMutable Value Semantics and inout Access
  939. Theorem 50.1 — Region inference refines Milner typingCapability and Region Types for Typed Memory Management
  940. Theorem 50.2 — Tofte–Talpin semantic correspondenceCapability and Region Types for Typed Memory Management
  941. Lemma 50.4 — Capability–memory correspondenceCapability and Region Types for Typed Memory Management
  942. Theorem 50.5 — Capability preservation and progressCapability and Region Types for Typed Memory Management
  943. Corollary 50.6 — Capability-calculus memory safetyCapability and Region Types for Typed Memory Management
  944. Theorem 50.7 — Complete collectionCapability and Region Types for Typed Memory Management
  945. Theorem 50.8 — Region-to-capability CPS type preservationCapability and Region Types for Typed Memory Management
  946. Theorem 50.10 — Core L^3 soundnessCapability and Region Types for Typed Memory Management
  947. Theorem 50.12 — Linear-region safetyCapability and Region Types for Typed Memory Management
  948. Theorem 50.14 — Monadic-region soundnessCapability and Region Types for Typed Memory Management
  949. Lemma 51.2 — Subcapturing preorderCapture Types and Capture-Set Polymorphism
  950. Lemma 51.3 — Finite subcapturing decompositionCapture Types and Capture-Set Polymorphism
  951. Lemma 51.4 — Covariant capture substitutionCapture Types and Capture-Set Polymorphism
  952. Lemma 51.5 — Capture bound of a valueCapture Types and Capture-Set Polymorphism
  953. Lemma 51.6 — Value substitutionCapture Types and Capture-Set Polymorphism
  954. Theorem 51.7 — Preservation and progress forCapture Types and Capture-Set Polymorphism
  955. Theorem 51.8 — Capture predictionCapture Types and Capture-Set Polymorphism
  956. Theorem 51.9 — Mechanized boxed-state safetyCapture Types and Capture-Set Polymorphism
  957. Lemma 52.2 — One-step state preservationTypestate and State-Transition Protocols
  958. Lemma 52.3 — Protocol progressTypestate and State-Transition Protocols
  959. Theorem 52.4 — Protocol safetyTypestate and State-Transition Protocols
  960. Lemma 53.1 — Flat call-by-value substitutionCoeffects and Context-Dependent Computation
  961. Theorem 53.2 — Flat call-by-value subject reductionCoeffects and Context-Dependent Computation
  962. Lemma 53.3 — Top-pointed substitutionCoeffects and Context-Dependent Computation
  963. Lemma 53.4 — Bottom-pointed substitutionCoeffects and Context-Dependent Computation
  964. Theorem 53.5 — Flat call-by-name subject reductionCoeffects and Context-Dependent Computation
  965. Lemma 53.6 — Structural substitutionCoeffects and Context-Dependent Computation
  966. Theorem 53.7 — Structural subject reductionCoeffects and Context-Dependent Computation
  967. Lemma 54.2 — Graded substitutionTwo Bases for Graded Types: Calculi and Correspondence
  968. Theorem 54.3 — Graded-to-linear correspondenceTwo Bases for Graded Types: Calculi and Correspondence
  969. Corollary 54.4 — Grade preservationTwo Bases for Graded Types: Calculi and Correspondence
  970. Theorem 54.5 — Linear-to-graded CPS correspondenceTwo Bases for Graded Types: Calculi and Correspondence
  971. Lemma 54.6 — Two substitution principlesTwo Bases for Graded Types: Calculi and Correspondence
  972. Theorem 54.7 — Equational soundness of combined gradingTwo Bases for Graded Types: Calculi and Correspondence
  973. Theorem 54.8 — Fractional-uniqueness safety packageTwo Bases for Graded Types: Calculi and Correspondence
  974. Proposition 55.1 — No old-heap reachabilityTemporal Types and Functional Reactive Programming
  975. Theorem 55.2 — Fundamental Property, Simply RaTT Theorem 6.3Temporal Types and Functional Reactive Programming
  976. Theorem 55.3 — Productivity, Simply RaTT Theorem 3.1Temporal Types and Functional Reactive Programming
  977. Theorem 55.4 — Causality, Simply RaTT Theorem 3.2Temporal Types and Functional Reactive Programming
  978. Lemma 56.2 — External reduction decreases weightSoft Linear Logic and Implicit Complexity
  979. Theorem 56.3 — Normalization invariant, Lafont Theorem 2Soft Linear Logic and Implicit Complexity
  980. Corollary 56.4 — Fixed-net polynomialSoft Linear Logic and Implicit Complexity
  981. Theorem 56.5 — Polynomial predicate representation, Lafont Theorem 9Soft Linear Logic and Implicit Complexity
  982. Lemma 57.1 — Head–tail identityAmortized Resource Analysis and Typed Potentials
  983. Lemma 57.2 — Potential splits and weakensAmortized Resource Analysis and Typed Potentials
  984. Theorem 57.3 — Hoffmann–Hofmann soundnessAmortized Resource Analysis and Typed Potentials
  985. Theorem 58.1 — Type preservation for the selected calculusBinary Session Types and Typed Protocols
  986. Theorem 58.2 — Closed progress for the selected calculusBinary Session Types and Typed Protocols
  987. Lemma 58.3 — Unfolding and dualityBinary Session Types and Typed Protocols
  988. Theorem 58.4 — Journal progress and preservation cardBinary Session Types and Typed Protocols
  989. Theorem 59.4 — Repaired subject reductionMultiparty and Asynchronous Session Types
  990. Corollary 59.5 — Communication safetyMultiparty and Asynchronous Session Types
  991. Theorem 59.7 — Pirouette relative type soundnessMultiparty and Asynchronous Session Types
  992. Theorem 59.8 — Pirouette projection cardMultiparty and Asynchronous Session Types
  993. Lemma 60.6 — Monotonicity in product triplesThe Lambda Cube and Pure Type Systems
  994. Proposition 60.7 — Recovery of the familiar systemsThe Lambda Cube and Pure Type Systems
  995. Lemma 60.10 — Context validityThe Lambda Cube and Pure Type Systems
  996. Lemma 60.11 — Free variablesThe Lambda Cube and Pure Type Systems
  997. Lemma 60.12 — Composition of substitutionThe Lambda Cube and Pure Type Systems
  998. Lemma 60.13 — Beta-equivalence and substitutionThe Lambda Cube and Pure Type Systems
  999. Lemma 60.14 — WeakeningThe Lambda Cube and Pure Type Systems
  1000. Theorem 60.15 — SubstitutionThe Lambda Cube and Pure Type Systems
  1001. Lemma 60.16 — GenerationThe Lambda Cube and Pure Type Systems
  1002. Lemma 60.17 — Correctness of typesThe Lambda Cube and Pure Type Systems
  1003. Lemma 60.18 — Confluence of beta-reduction on pseudo-termsThe Lambda Cube and Pure Type Systems
  1004. Corollary 60.19 — Church–RosserThe Lambda Cube and Pure Type Systems
  1005. Lemma 60.20 — Product compatibilityThe Lambda Cube and Pure Type Systems
  1006. Theorem 60.21 — Subject reductionThe Lambda Cube and Pure Type Systems
  1007. Corollary 60.22 — Legality under declaration reductionThe Lambda Cube and Pure Type Systems
  1008. Theorem 60.23 — Strong normalization of the lambda cubeThe Lambda Cube and Pure Type Systems
  1009. Theorem 60.24 — Girard's boundary for the one-sort PTSThe Lambda Cube and Pure Type Systems
  1010. Lemma 60.26 — Uniqueness of types modulo betaThe Lambda Cube and Pure Type Systems
  1011. Theorem 60.27 — Conditional decidable checkingThe Lambda Cube and Pure Type Systems
  1012. Proposition 60.28 — What a cube placement does not establishThe Lambda Cube and Pure Type Systems
  1013. Theorem 61.4 — Canonical forms for LFLogical Frameworks, Encodings, and Adequacy
  1014. Lemma 61.6 — Proposition-code inversionLogical Frameworks, Encodings, and Adequacy
  1015. Lemma 61.9 — Compositionality of the implication encodingLogical Frameworks, Encodings, and Adequacy
  1016. Theorem 61.10 — Adequacy for implicational natural deductionLogical Frameworks, Encodings, and Adequacy
  1017. Lemma 61.13 — STLC representation commutes with substitutionLogical Frameworks, Encodings, and Adequacy
  1018. Lemma 61.14 — STLC type-code inversionLogical Frameworks, Encodings, and Adequacy
  1019. Lemma 61.15 — No exotic STLC inhabitantsLogical Frameworks, Encodings, and Adequacy
  1020. Theorem 61.16 — Adequacy for intrinsically typed STLCLogical Frameworks, Encodings, and Adequacy
  1021. Proposition 61.17 — Framework trust and adequacy obligationsLogical Frameworks, Encodings, and Adequacy
  1022. Lemma 61.18 — Weakening commutes with de Bruijn substitutionLogical Frameworks, Encodings, and Adequacy
  1023. Lemma 61.19 — De Bruijn substitution lawsLogical Frameworks, Encodings, and Adequacy
  1024. Lemma 61.20 — Opening commutes with free substitutionLogical Frameworks, Encodings, and Adequacy
  1025. Lemma 61.21 — Locally nameless substitutionLogical Frameworks, Encodings, and Adequacy
  1026. Theorem 61.24 — PHOAS renaming, substitution, and preservationLogical Frameworks, Encodings, and Adequacy
  1027. Proposition 61.25 — Contextual substitutionLogical Frameworks, Encodings, and Adequacy
  1028. Theorem 61.26 — One obligation, four proofsLogical Frameworks, Encodings, and Adequacy
  1029. Proposition 61.28 — Adequacy is signature-relativeLogical Frameworks, Encodings, and Adequacy
  1030. Proposition 62.3 — Least finite supportNominal Syntax, Support, and Binding
  1031. Lemma 62.5 — Fresh comparison of abstractionsNominal Syntax, Support, and Binding
  1032. Proposition 62.6 — Support of name abstractionNominal Syntax, Support, and Binding
  1033. Lemma 62.7 — Fresh representativeNominal Syntax, Support, and Binding
  1034. Lemma 62.9 — Typing equivarianceNominal Syntax, Support, and Binding
  1035. Theorem 62.10 — Freshness inductionNominal Syntax, Support, and Binding
  1036. Theorem 62.11 — Freshness recursionNominal Syntax, Support, and Binding
  1037. Lemma 62.13 — Nominal substitution and typingNominal Syntax, Support, and Binding
  1038. Theorem 62.14 — Nominal adequacy for STLCNominal Syntax, Support, and Binding
  1039. Proposition 62.15 — Nominal and de Bruijn comparisonNominal Syntax, Support, and Binding
  1040. Lemma 62.17 — Support of nominal substitutionNominal Syntax, Support, and Binding
  1041. Proposition 62.19 — Nominal substitution squareNominal Syntax, Support, and Binding
  1042. Proposition 63.3 — Ordinary and contextual substitutionContextual Modal Type Theory and Beluga
  1043. Theorem 63.4 — Simply typed CMTT metatheoryContextual Modal Type Theory and Beluga
  1044. Theorem 63.6 — Qualified hereditary substitution and decidabilityContextual Modal Type Theory and Beluga
  1045. Proposition 63.7 — Context preservation of eta expansionContextual Modal Type Theory and Beluga
  1046. Proposition 63.9 — Paired-block scope invariantContextual Modal Type Theory and Beluga
  1047. Lemma 64.1 — Fresh atoms existDependent Nominal Type Theory
  1048. Lemma 64.2 — Support of abstractionDependent Nominal Type Theory
  1049. Lemma 64.3 — Restriction is deterministicDependent Nominal Type Theory
  1050. Lemma 64.4 — Substitution restrictionDependent Nominal Type Theory
  1051. Theorem 64.5 — General substitutionDependent Nominal Type Theory
  1052. Theorem 64.6 — Soundness of algorithmic equivalenceDependent Nominal Type Theory
  1053. Lemma 64.7 — Fundamental logical-relation lemmaDependent Nominal Type Theory
  1054. Lemma 64.8 — Logical implies algorithmicDependent Nominal Type Theory
  1055. Theorem 64.9 — Completeness and decidabilityDependent Nominal Type Theory
  1056. Theorem 64.10 — Canonicalization and conservativityDependent Nominal Type Theory
  1057. Theorem 64.11 — Adequacy of the nominal encodingDependent Nominal Type Theory
  1058. Theorem 64.12 — Adequacy of explicit alpha-inequalityDependent Nominal Type Theory
  1059. Lemma 65.1 — Semantic substitutionClassical Simple Type Theory and HOL
  1060. Theorem 65.2 — Kernel soundnessClassical Simple Type Theory and HOL
  1061. Corollary 65.3Classical Simple Type Theory and HOL
  1062. Theorem 65.4 — LCF confinementClassical Simple Type Theory and HOL
  1063. Lemma 66.1 — Reducibility of primitive recursionSystem T and the Dialectica Interpretation
  1064. Theorem 66.2 — Fundamental theoremSystem T and the Dialectica Interpretation
  1065. Corollary 66.3 — Normalization and numerical canonicitySystem T and the Dialectica Interpretation
  1066. Lemma 66.4 — Deciding a matrixSystem T and the Dialectica Interpretation
  1067. Theorem 66.5 — Dialectica soundness for HASystem T and the Dialectica Interpretation
  1068. Lemma 67.4 — Finite product equationsBar Recursion, Choice, and Program Extraction
  1069. Theorem 67.5 — Finite DNS and finite choiceBar Recursion, Choice, and Program Extraction
  1070. Proposition 67.6 — Exact finite-type levelBar Recursion, Choice, and Program Extraction
  1071. Proposition 67.7 — No uniform coordinate horizonBar Recursion, Choice, and Program Extraction
  1072. Lemma 67.9 — Prefix factorizationBar Recursion, Choice, and Program Extraction
  1073. Theorem 67.10 — Controlled-product equationsBar Recursion, Choice, and Program Extraction
  1074. Theorem 67.13 — The controlled product defines SBRBar Recursion, Choice, and Program Extraction
  1075. Theorem 67.14 — Conditional reverse definabilityBar Recursion, Choice, and Program Extraction
  1076. Lemma 67.15 — Spector's conditionBar Recursion, Choice, and Program Extraction
  1077. Theorem 67.16 — Totality of restricted Spector recursionBar Recursion, Choice, and Program Extraction
  1078. Theorem 67.17 — Spector equationsBar Recursion, Choice, and Program Extraction
  1079. Theorem 67.18 — Selected choice interpretationBar Recursion, Choice, and Program Extraction
  1080. Theorem 68.2 — Fixed-point characterization of reachabilityAbstract Interpretation, Type Systems, and Verified Static Analysis
  1081. Lemma 68.3 — Sign Galois insertionAbstract Interpretation, Type Systems, and Verified Static Analysis
  1082. Lemma 68.4 — Local soundness of signsAbstract Interpretation, Type Systems, and Verified Static Analysis
  1083. Lemma 68.6 — Consequences of the adjunctionAbstract Interpretation, Type Systems, and Verified Static Analysis
  1084. Theorem 68.7 — Best correct approximationAbstract Interpretation, Type Systems, and Verified Static Analysis
  1085. Lemma 68.8 — Interval Galois insertionAbstract Interpretation, Type Systems, and Verified Static Analysis
  1086. Theorem 68.10 — Compositional analyzer soundnessAbstract Interpretation, Type Systems, and Verified Static Analysis
  1087. Theorem 68.11 — Fixed-point transferAbstract Interpretation, Type Systems, and Verified Static Analysis
  1088. Theorem 68.13 — Widening coverage and terminationAbstract Interpretation, Type Systems, and Verified Static Analysis
  1089. Lemma 68.14 — Sound reduction with intervalsAbstract Interpretation, Type Systems, and Verified Static Analysis
  1090. Corollary 68.15 — Countdown safetyAbstract Interpretation, Type Systems, and Verified Static Analysis
  1091. Theorem 68.16 — Move borrow-graph preservationAbstract Interpretation, Type Systems, and Verified Static Analysis
  1092. Theorem 68.17 — Type safety from abstractionAbstract Interpretation, Type Systems, and Verified Static Analysis
  1093. Theorem 68.18 — Abstract-machine simulationAbstract Interpretation, Type Systems, and Verified Static Analysis
  1094. Lemma 68.20 — Constructive calculation of a transformerAbstract Interpretation, Type Systems, and Verified Static Analysis
  1095. Theorem 68.21 — Extracted analyzer boundaryAbstract Interpretation, Type Systems, and Verified Static Analysis
  1096. Theorem 68.22 — Verasco's exact safety conclusionAbstract Interpretation, Type Systems, and Verified Static Analysis
  1097. Proposition 68.24 — Neither target is a renaming of the otherAbstract Interpretation, Type Systems, and Verified Static Analysis
  1098. Theorem 68.25 — Sound unnormalized measure boundsAbstract Interpretation, Type Systems, and Verified Static Analysis
  1099. Lemma 69.1 — Expression correspondenceSymbolic Execution, Path Conditions, and Concolic Testing
  1100. Theorem 69.3 — One-step simulationSymbolic Execution, Path Conditions, and Concolic Testing
  1101. Corollary 69.4 — Finite simulation and path soundnessSymbolic Execution, Path Conditions, and Concolic Testing
  1102. Theorem 69.5 — Loop-free finite-path coverageSymbolic Execution, Path Conditions, and Concolic Testing
  1103. Lemma 69.6 — Negative-cycle certificate soundnessSymbolic Execution, Path Conditions, and Concolic Testing
  1104. Theorem 69.7 — Certificate-checked pruning preserves coverageSymbolic Execution, Path Conditions, and Concolic Testing
  1105. Theorem 69.8 — Model-to-test correctnessSymbolic Execution, Path Conditions, and Concolic Testing
  1106. Proposition 69.9 — Subsumption soundnessSymbolic Execution, Path Conditions, and Concolic Testing
  1107. Proposition 69.10 — Guarded-merge representationSymbolic Execution, Path Conditions, and Concolic Testing
  1108. Theorem 69.11 — Concolic alternate-input justificationSymbolic Execution, Path Conditions, and Concolic Testing
  1109. Lemma 70.2 — Program-counter monotonicityInformation-Flow Type Systems and Noninterference
  1110. Proposition 70.3 — Subject reductionInformation-Flow Type Systems and Noninterference
  1111. Lemma 70.4 — Expression agreement, or simple securityInformation-Flow Type Systems and Noninterference
  1112. Lemma 70.5 — High-context confinementInformation-Flow Type Systems and Noninterference
  1113. Theorem 70.6 — Termination-insensitive noninterferenceInformation-Flow Type Systems and Noninterference
  1114. Theorem 70.7 — Original-DCC noninterferenceInformation-Flow Type Systems and Noninterference
  1115. Lemma 26.5 — Free variables after fresh renamingThe Rules of Dependent Type Theory
  1116. Proposition 26.7The Rules of Dependent Type Theory
  1117. Lemma 26.9 — Synchronized fresh displaysThe Rules of Dependent Type Theory
  1118. Proposition 26.11The Rules of Dependent Type Theory
  1119. Proposition 26.24 — SanityThe Rules of Dependent Type Theory
  1120. Proposition 26.25 — Characterization of contextsThe Rules of Dependent Type Theory
  1121. Corollary 26.26 — Context inversionThe Rules of Dependent Type Theory
  1122. Lemma 26.27 — The common context for equal substitutionThe Rules of Dependent Type Theory
  1123. Lemma 71.31 — Context peelingThe Rules of Dependent Type Theory
  1124. Lemma 26.30 — Change of variablesThe Rules of Dependent Type Theory
  1125. Lemma 71.33 — Substitute while retaining the source declarationThe Rules of Dependent Type Theory
  1126. Lemma 26.31 — Element conversionThe Rules of Dependent Type Theory
  1127. Lemma 26.32 — Equality conversionThe Rules of Dependent Type Theory
  1128. Lemma 26.33 — InterchangeThe Rules of Dependent Type Theory
  1129. Lemma 26.34 — General variable ruleThe Rules of Dependent Type Theory
  1130. Lemma 26.38 — Regularity and weakeningThe Rules of Dependent Type Theory
  1131. Lemma 26.39 — Ordinary substitution in the economical presentationThe Rules of Dependent Type Theory
  1132. Lemma 26.40 — Context conversion in the economical presentationThe Rules of Dependent Type Theory
  1133. Lemma 26.41 — Equal substitution in the economical presentationThe Rules of Dependent Type Theory
  1134. Corollary 26.42 — Simultaneous structural admissibilityThe Rules of Dependent Type Theory
  1135. Theorem 26.43 — Equivalence of presentationsThe Rules of Dependent Type Theory
  1136. Proposition 26.46 — Substitution by a contextThe Rules of Dependent Type Theory
  1137. Proposition 71.51 — Identity and composition of telescope mapsThe Rules of Dependent Type Theory
  1138. Lemma 27.7 — Category lawsDependent Products, Sums, and Unit
  1139. Proposition 27.8 — Evaluation-style eliminationDependent Products, Sums, and Unit
  1140. Proposition 27.12 — Σ -eliminationDependent Products, Sums, and Unit
  1141. Proposition 27.13 — The positive presentationDependent Products, Sums, and Unit
  1142. Lemma 27.15 — Scoping in the extended theoryDependent Products, Sums, and Unit
  1143. Proposition 27.17 — The dependent eliminator forDependent Products, Sums, and Unit
  1144. Proposition 27.20 — term classesDependent Products, Sums, and Unit
  1145. Theorem 27.21 — Π internalizes the hypothetical judgmentDependent Products, Sums, and Unit
  1146. Theorem 27.22 — Σ internalizes pairs of judgmentsDependent Products, Sums, and Unit
  1147. Proposition 27.25 — CurryingDependent Products, Sums, and Unit
  1148. Proposition 27.26 — Associativity of ΣDependent Products, Sums, and Unit
  1149. Lemma 27.28 — Calculus of definitional isomorphismsDependent Products, Sums, and Unit
  1150. Lemma 28.13 — Semantic substitution and weakeningInductive Types
  1151. Lemma 73.15 — Soundness through booleansInductive Types
  1152. Proposition 28.15 — A separating set interpretationInductive Types
  1153. Theorem 28.26 — Logical readingInductive Types
  1154. Theorem 28.32 — Encodings via W-typesInductive Types
  1155. Lemma 28.14 — Soundness of the partial interpretationInductive Types
  1156. Corollary 73.41 — Relative consistency of the inductive fragmentInductive Types
  1157. Proposition 73.44 — Set soundness of the polynomial schemaInductive Types
  1158. Proposition 73.48 — Rule-set interpretationInductive Types
  1159. Lemma 73.50 — Bridge from constant-telescope signaturesInductive Types
  1160. Lemma 73.51 — Container normal formInductive Types
  1161. Theorem 73.52 — Dybjer's W-representation theoremInductive Types
  1162. Proposition 29.16 — Families are maps intoUniverses and Universe Levels
  1163. Proposition 74.10 — Completeness of the normalized solverUniverses and Universe Levels
  1164. Lemma 74.14 — Set interpretation of the universe rulesUniverses and Universe Levels
  1165. Theorem 74.15 — Relative consistency and separationUniverses and Universe Levels
  1166. Theorem 29.14 — Disjointness of the booleansUniverses and Universe Levels
  1167. Lemma 75.3 — Code substitutionTarski Universes and Decoding
  1168. Theorem 75.6 — The strict comparisonTarski Universes and Decoding
  1169. Lemma 76.3 — The three inhabitantsUniverse Paradoxes and Hurkens's Construction
  1170. Theorem 76.4 — Hurkens collapseUniverse Paradoxes and Hurkens's Construction
  1171. Corollary 76.5 — The exact inconsistency boundaryUniverse Paradoxes and Hurkens's Construction
  1172. Theorem 76.6 — Reynolds–Hurkens retraction boundaryUniverse Paradoxes and Hurkens's Construction
  1173. Lemma 30.4 — Judgmental equality yields identificationsIdentity Types
  1174. Proposition 30.11 — Indiscernibility of identicalsIdentity Types
  1175. Proposition 30.13 — Least reflexive relationIdentity Types
  1176. Theorem 30.20 — Groupoid lawsIdentity Types
  1177. Proposition 30.21 — Functoriality ofIdentity Types
  1178. Proposition 30.22 — Transport is functorialIdentity Types
  1179. Theorem 30.26 — Based path inductionIdentity Types
  1180. Proposition 30.27 — Equivalence of the presentationsIdentity Types
  1181. Proposition 30.29Identity Types
  1182. Proposition 77.32 — The set interpretation validates UIP and function extensionalityIdentity Types
  1183. Theorem 78.4 — The two finite families agreeIndexed Inductive Families and Dependent Pattern Matching
  1184. Proposition 78.6 — No confusion used for vectors and finite indicesIndexed Inductive Families and Dependent Pattern Matching
  1185. Lemma 78.12 — No-confusion retractionIndexed Inductive Families and Dependent Pattern Matching
  1186. Lemma 78.14 — Acyclicity of recursive descentIndexed Inductive Families and Dependent Pattern Matching
  1187. Lemma 78.16 — Proof-relevant specializationIndexed Inductive Families and Dependent Pattern Matching
  1188. Lemma 78.17 — One case-tree split is eliminableIndexed Inductive Families and Dependent Pattern Matching
  1189. Theorem 78.19 — Elimination of valid dependent case treesIndexed Inductive Families and Dependent Pattern Matching
  1190. Lemma 79.2 — Record substitutionDependent Records and Primitive Projections
  1191. Theorem 79.3 — The exact Sigma comparisonDependent Records and Primitive Projections
  1192. Theorem 79.4 — Pollack-to-CPT correspondenceDependent Records and Primitive Projections
  1193. Theorem 79.5 — Checking and available canonicity for recordsDependent Records and Primitive Projections
  1194. Lemma 80.5 — Interpretation functor lawsUniverses of Datatype Descriptions and Generic Programs
  1195. Lemma 80.6 — Congruence of description actionUniverses of Datatype Descriptions and Generic Programs
  1196. Lemma 80.7 — Layer-local congruenceUniverses of Datatype Descriptions and Generic Programs
  1197. Lemma 80.9 — Fold calculationUniverses of Datatype Descriptions and Generic Programs
  1198. Theorem 80.11 — Fold fusionUniverses of Datatype Descriptions and Generic Programs
  1199. Lemma 80.13 — An immediate recursive child is smallerUniverses of Datatype Descriptions and Generic Programs
  1200. Lemma 80.17 — Composite applicative lawsUniverses of Datatype Descriptions and Generic Programs
  1201. Proposition 80.19 — Traversal lawsUniverses of Datatype Descriptions and Generic Programs
  1202. Lemma 80.22 — Decidable equality gives local UIPUniverses of Datatype Descriptions and Generic Programs
  1203. Theorem 80.23 — Generic decidable equalityUniverses of Datatype Descriptions and Generic Programs
  1204. Theorem 80.25 — Soundness of the displayed elaborationUniverses of Datatype Descriptions and Generic Programs
  1205. Lemma 80.27 — Binding-layer action lawsUniverses of Datatype Descriptions and Generic Programs
  1206. Theorem 80.28 — Generic renaming and substitution lawsUniverses of Datatype Descriptions and Generic Programs
  1207. Proposition 81.3 — Container action lawsContainers, Polynomial Functors, and Ornaments
  1208. Theorem 81.9 — Conditional fold and unfold lawsContainers, Polynomial Functors, and Ornaments
  1209. Theorem 81.12 — Indexed-container representation, source signatureContainers, Polynomial Functors, and Ornaments
  1210. Proposition 81.14 — Plugging one holeContainers, Polynomial Functors, and Ornaments
  1211. Theorem 81.15 — Derivative laws at the decidable-container boundaryContainers, Polynomial Functors, and Ornaments
  1212. Proposition 81.18 — Transported map coherenceContainers, Polynomial Functors, and Ornaments
  1213. Proposition 81.19 — The append lifting preserves the ML ornamentContainers, Polynomial Functors, and Ornaments
  1214. Theorem 82.5 — Accessibility inductionWell-Founded Recursion
  1215. Proposition 82.7 — Extensional independence of certificatesWell-Founded Recursion
  1216. Lemma 82.11 — Natural-order inversion and mixed transitivityWell-Founded Recursion
  1217. Lemma 82.12 — Natural-number accessibilityWell-Founded Recursion
  1218. Theorem 82.14 — Measure recursionWell-Founded Recursion
  1219. Theorem 82.16 — Lexicographic well-foundednessWell-Founded Recursion
  1220. Lemma 82.17 — Natural arithmetic interfaceWell-Founded Recursion
  1221. Lemma 82.18 — Natural-number divisionWell-Founded Recursion
  1222. Theorem 82.20 — Euclid equations and terminationWell-Founded Recursion
  1223. Theorem 82.22 — Common-divisor specificationWell-Founded Recursion
  1224. Theorem 82.25 — The division domain is totalWell-Founded Recursion
  1225. Lemma 83.5 — Truthful compositionSize-Change Termination
  1226. Theorem 83.8 — Size-change descentSize-Change Termination
  1227. Lemma 83.10 — A strict diagonal repeatsSize-Change Termination
  1228. Theorem 83.11 — Finite idempotent criterionSize-Change Termination
  1229. Corollary 83.12 — Sound finite checkerSize-Change Termination
  1230. Proposition 84.3 — Ordinary folds are Mendler foldsMendler Recursion, Nested Datatypes, and Mixed Variance
  1231. Lemma 84.4 — Abstract-domain confinementMendler Recursion, Nested Datatypes, and Mixed Variance
  1232. Theorem 84.5 — Mendler iteration normalization, importedMendler Recursion, Nested Datatypes, and Mixed Variance
  1233. Proposition 84.7 — Renaming fusionMendler Recursion, Nested Datatypes, and Mixed Variance
  1234. Lemma 84.10 — Rename after lifted substitutionMendler Recursion, Nested Datatypes, and Mixed Variance
  1235. Proposition 84.11 — Renaming–substitution fusionMendler Recursion, Nested Datatypes, and Mixed Variance
  1236. Proposition 84.13 — Dependent Mendler inductionMendler Recursion, Nested Datatypes, and Mixed Variance
  1237. Theorem 84.14 — Hierarchy boundary, importedMendler Recursion, Nested Datatypes, and Mixed Variance
  1238. Theorem 84.16 — Constraint normalization, importedMendler Recursion, Nested Datatypes, and Mixed Variance
  1239. Theorem 85.3 — Productivity of guarded corecursionCoinduction, Copatterns, and Bisimulation
  1240. Lemma 85.7 — Successor iterate swapCoinduction, Copatterns, and Bisimulation
  1241. Proposition 85.8 — Fibonacci recurrenceCoinduction, Copatterns, and Bisimulation
  1242. Theorem 85.13 — Stream coinductionCoinduction, Copatterns, and Bisimulation
  1243. Theorem 85.15 — Map fusionCoinduction, Copatterns, and Bisimulation
  1244. Lemma 85.16 — Zip observationsCoinduction, Copatterns, and Bisimulation
  1245. Corollary 85.17 — The feedback equation for FibonacciCoinduction, Copatterns, and Bisimulation
  1246. Theorem 85.19 — Finite-observation productivity for the schemaCoinduction, Copatterns, and Bisimulation
  1247. Theorem 85.24 — Bounded observation calculationCoinduction, Copatterns, and Bisimulation
  1248. Theorem 86.5 — Weak equivalence lawsRecursive Effects and Interaction Trees
  1249. Theorem 86.6 — Bind congruence and associativityRecursive Effects and Interaction Trees
  1250. Theorem 86.8 — Interpreter identity and compositionRecursive Effects and Interaction Trees
  1251. Theorem 86.11 — Successor-server prefixRecursive Effects and Interaction Trees
  1252. Lemma 87.5 — Module and linking algebraCompositional Linearizability and Modular Concurrent Objects
  1253. Theorem 87.7 — Observational refinement and localityCompositional Linearizability and Modular Concurrent Objects
  1254. Theorem 87.8 — Horizontal and vertical compositionCompositional Linearizability and Modular Concurrent Objects
  1255. Theorem 87.9 — Restricted set specializationCompositional Linearizability and Modular Concurrent Objects
  1256. Proposition 88.4 — The ambiguous-queue pruning calculationPossibility Reasoning and Linearizability Hoare Logic
  1257. Lemma 88.7 — Rely preservationPossibility Reasoning and Linearizability Hoare Logic
  1258. Theorem 88.9 — Generic lock protectionPossibility Reasoning and Linearizability Hoare Logic
  1259. Theorem 88.10 — Soundness of LHLPossibility Reasoning and Linearizability Hoare Logic
  1260. Theorem 88.11 — Artifact-faithful semantic completenessPossibility Reasoning and Linearizability Hoare Logic
  1261. Theorem 89.19 — Imported: confluence of historical reductionThe Calculus of Inductive Constructions
  1262. Theorem 89.21 — Conditional checker endpointThe Calculus of Inductive Constructions
  1263. Proposition 35.4 — A separating set interpretationExtensional Type Theory
  1264. Corollary 90.7 — Relative consistencyExtensional Type Theory
  1265. Theorem 35.7 — Eq internalizes judgmental equalityExtensional Type Theory
  1266. Theorem 35.9 — Consequences of reflectionExtensional Type Theory
  1267. Proposition 35.10 — Collapse of the identity typeExtensional Type Theory
  1268. Corollary 35.11 — The groupoid structure trivializesExtensional Type Theory
  1269. Lemma 35.15 — Closure propertiesExtensional Type Theory
  1270. Lemma 35.16 — Internal characterizationExtensional Type Theory
  1271. Corollary 35.19 — Set interpretation of truncationExtensional Type Theory
  1272. Proposition 35.21 — Dependent truncation eliminationExtensional Type Theory
  1273. Proposition 35.23 — The logic of ETTExtensional Type Theory
  1274. Lemma 35.28 — Stripping and bindingExtensional Type Theory
  1275. Proposition 35.29 — Soundness of strippingExtensional Type Theory
  1276. Lemma 35.30 — General UIP in T_IExtensional Type Theory
  1277. Lemma 35.32 — Equal-substitution transportExtensional Type Theory
  1278. Lemma 35.34 — Canonical comparisons for the formersExtensional Type Theory
  1279. Lemma 35.36 — Quotient substitution and comprehensionExtensional Type Theory
  1280. Lemma 35.37 — The formers and eliminators descendExtensional Type Theory
  1281. Lemma 35.38 — The quotient model and its triangleExtensional Type Theory
  1282. Theorem 35.39 — Conservativity; HofmannExtensional Type Theory
  1283. Theorem 90.48 — Imported: Kapulkin–Li Morita equivalenceExtensional Type Theory
  1284. Lemma 35.44 — The SK word problem is undecidableExtensional Type Theory
  1285. Lemma 35.46 — Soundness of the encodingExtensional Type Theory
  1286. Lemma 35.47 — Completeness of the encodingExtensional Type Theory
  1287. Lemma 35.48 — Generation for equality formationExtensional Type Theory
  1288. Theorem 35.49 — UndecidabilityExtensional Type Theory
  1289. Theorem 91.8 — The closure assigns PERsNuprl-Style Computational Type Theory and Realizability
  1290. Lemma 91.10 — Finite compatible reduction preserves lazy observationsNuprl-Style Computational Type Theory and Realizability
  1291. Lemma 91.11 — Coherence of frozen computationNuprl-Style Computational Type Theory and Realizability
  1292. Theorem 91.12 — Computational stability of closure and membersNuprl-Style Computational Type Theory and Realizability
  1293. Corollary 91.13 — Canonical-form closure inversion and PER transportNuprl-Style Computational Type Theory and Realizability
  1294. Proposition 91.15 — Universe classification and cumulative persistenceNuprl-Style Computational Type Theory and Realizability
  1295. Lemma 91.17 — The derived natural is a typeNuprl-Style Computational Type Theory and Realizability
  1296. Theorem 91.18 — Meaning and canonicity of derived naturalsNuprl-Style Computational Type Theory and Realizability
  1297. Lemma 91.20 — Endpoints of equal substitutionsNuprl-Style Computational Type Theory and Realizability
  1298. Theorem 91.23 — Equivalence of the two pinned sequent meaningsNuprl-Style Computational Type Theory and Realizability
  1299. Proposition 91.25 — Local list and substitution correspondenceNuprl-Style Computational Type Theory and Realizability
  1300. Theorem 91.26 — Dependent function and pair rulesNuprl-Style Computational Type Theory and Realizability
  1301. Theorem 91.27 — Equality and set rulesNuprl-Style Computational Type Theory and Realizability
  1302. Lemma 91.28 — Natural hypothesis and successor closureNuprl-Style Computational Type Theory and Realizability
  1303. Theorem 91.30 — The successor program meets its set specificationNuprl-Style Computational Type Theory and Realizability
  1304. Theorem 91.31 — Successor theorem and extracted programNuprl-Style Computational Type Theory and Realizability
  1305. Theorem 91.32 — Computational consistencyNuprl-Style Computational Type Theory and Realizability
  1306. Lemma 91.35 — Quotient-compatible observation stabilityNuprl-Style Computational Type Theory and Realizability
  1307. Lemma 91.37 — Old-stratum inhabitance persistenceNuprl-Style Computational Type Theory and Realizability
  1308. Theorem 91.38 — Quotient-extension invariants and well-definednessNuprl-Style Computational Type Theory and Realizability
  1309. Proposition 91.39 — Displayed quotient rulesNuprl-Style Computational Type Theory and Realizability
  1310. Theorem 92.5 — Displayed conservativity pairLogic-Enriched Type Theory and Predicative Mathematics
  1311. Lemma 93.3 — Erasure commutes with substitutionDependent Intersections and Same-Subject Refinement
  1312. Lemma 93.4 — SubstitutionDependent Intersections and Same-Subject Refinement
  1313. Theorem 93.5 — Erasure preservationDependent Intersections and Same-Subject Refinement
  1314. Theorem 93.6 — Kopylov semantic validationDependent Intersections and Same-Subject Refinement
  1315. Lemma 94.4 — Constructor typingSubject-Dependent Self Types
  1316. Theorem 94.5 — Derived natural-number inductionSubject-Dependent Self Types
  1317. Lemma 94.6 — System S substitutionSubject-Dependent Self Types
  1318. Theorem 94.7 — Confluence and preservationSubject-Dependent Self Types
  1319. Theorem 94.8 — Strong normalization of System SSubject-Dependent Self Types
  1320. Lemma 95.4 — Restriction commutes with substitutionVery Dependent Functions
  1321. Theorem 95.5 — Substitution for very-dependent functionsVery Dependent Functions
  1322. Theorem 95.6 — Soundness of the extracted rulesVery Dependent Functions
  1323. Proposition 95.7 — Width subtypingVery Dependent Functions
  1324. Theorem 96.4 — Derived inductionCDLE and Cedille: Lambda-Encoded Induction, Recursion, and Zero-Cost Reuse
  1325. Theorem 96.5 — Cedille Core soundness and consistencyCDLE and Cedille: Lambda-Encoded Induction, Recursion, and Zero-Cost Reuse
  1326. Theorem 96.6 — Derived monotone recursive typeCDLE and Cedille: Lambda-Encoded Induction, Recursion, and Zero-Cost Reuse
  1327. Theorem 96.7 — Simulated Nary computationCDLE and Cedille: Lambda-Encoded Induction, Recursion, and Zero-Cost Reuse
  1328. Lemma 97.3 — Typed substitutionThe lambda-Pi-Calculus Modulo Rewriting
  1329. Lemma 97.4 — A typed rule remains typed after matchingThe lambda-Pi-Calculus Modulo Rewriting
  1330. Theorem 97.5 — Subject reduction for the algebraic fragmentThe lambda-Pi-Calculus Modulo Rewriting
  1331. Theorem 97.6 — The conditional metatheorem chainThe lambda-Pi-Calculus Modulo Rewriting
  1332. Theorem 97.8 — Modulo-beta boundaryThe lambda-Pi-Calculus Modulo Rewriting
  1333. Theorem 97.9 — Adequacy for normal implicational derivationsThe lambda-Pi-Calculus Modulo Rewriting
  1334. Proposition 98.5 — Shape preservationLinear Dependent Type Theory
  1335. Theorem 98.6 — SubstitutionLinear Dependent Type Theory
  1336. Lemma 98.8 — Evaluation commutes with shapeLinear Dependent Type Theory
  1337. Proposition 98.9 — Preservation for evaluationLinear Dependent Type Theory
  1338. Theorem 98.11 — Imported interpretation packageLinear Dependent Type Theory
  1339. Lemma 98.12 — Imported semantic value substitutionLinear Dependent Type Theory
  1340. Theorem 98.13 — Soundness for LD^1Linear Dependent Type Theory
  1341. Lemma 99.3 — Zero needs nothingQuantitative Dependent Type Theory
  1342. Theorem 99.6 — Quantitative substitutionQuantitative Dependent Type Theory
  1343. Corollary 99.7 — Beta preservationQuantitative Dependent Type Theory
  1344. Proposition 99.8 — Zero-context boundaryQuantitative Dependent Type Theory
  1345. Theorem 100.8 — Graded substitutionGraded Modal Dependent Type Theory
  1346. Lemma 100.9 — Reduction gives typed equalityGraded Modal Dependent Type Theory
  1347. Theorem 100.10 — Type preservationGraded Modal Dependent Type Theory
  1348. Theorem 100.13 — Imported semantic typingGraded Modal Dependent Type Theory
  1349. Corollary 100.14 — Beta strong normalizationGraded Modal Dependent Type Theory
  1350. Theorem 101.6 — Usage substitution and preservationGraded Erasure and Extraction
  1351. Theorem 101.7 — Normalization and conversionGraded Erasure and Extraction
  1352. Lemma 101.10 — No extracted occurrenceGraded Erasure and Extraction
  1353. Theorem 101.11 — Operational erasure soundnessGraded Erasure and Extraction
  1354. Theorem 101.13 — Resource-correct numeral evaluationGraded Erasure and Extraction
  1355. Lemma 102.5 — Quantifier communication fidelityDependent Session Types and Protocol-Indexed Programming
  1356. Lemma 102.6 — Functional weakening and substitutionDependent Session Types and Protocol-Indexed Programming
  1357. Lemma 102.7 — Principal communicationDependent Session Types and Protocol-Indexed Programming
  1358. Theorem 102.8 — Type preservationDependent Session Types and Protocol-Indexed Programming
  1359. Theorem 102.9 — Closed global progressDependent Session Types and Protocol-Indexed Programming
  1360. Theorem 103.3 — Fire TriangleDependent Effects and Call-by-Push-Value
  1361. Lemma 103.7 — Value substitutionDependent Effects and Call-by-Push-Value
  1362. Lemma 103.9 — Equality-preserved classifiersDependent Effects and Call-by-Push-Value
  1363. Theorem 103.10 — Subject reductionDependent Effects and Call-by-Push-Value
  1364. Theorem 104.4 — CPS produces a Dijkstra monadWeakest Preconditions and Dijkstra Monads
  1365. Theorem 104.7 — Conditional WP soundness for total computationsWeakest Preconditions and Dijkstra Monads
  1366. Lemma 105.3 — Delay lawsPartiality and General Recursion in Dependent Type Theory
  1367. Lemma 105.5 — Bind convergencePartiality and General Recursion in Dependent Type Theory
  1368. Lemma 105.7 — Extensional return and bindPartiality and General Recursion in Dependent Type Theory
  1369. Theorem 105.8 — Partiality Kleisli triplePartiality and General Recursion in Dependent Type Theory
  1370. Theorem 105.9 — Search adequacyPartiality and General Recursion in Dependent Type Theory
  1371. Theorem 105.10 — Representability of partial-recursive presentationsPartiality and General Recursion in Dependent Type Theory
  1372. Theorem 105.12 — Finitary least fixed pointPartiality and General Recursion in Dependent Type Theory
  1373. Lemma 106.2 — Dependent application through subtypingDependent Subtyping, Refinement, and Graduality
  1374. Theorem 106.3 — λ P_≤ metatheoryDependent Subtyping, Refinement, and Graduality
  1375. Lemma 106.6 — Logical substitutionDependent Subtyping, Refinement, and Graduality
  1376. Lemma 106.7 — Refinement narrowing and substitutionDependent Subtyping, Refinement, and Graduality
  1377. Lemma 106.8 — Certified subtyping structureDependent Subtyping, Refinement, and Graduality
  1378. Theorem 106.9 — Correctness and completeness of principal checkingDependent Subtyping, Refinement, and Graduality
  1379. Theorem 106.10 — Preservation and decidability for DRefDependent Subtyping, Refinement, and Graduality
  1380. Theorem 106.13 — Fire triangle for gradual CICDependent Subtyping, Refinement, and Graduality
  1381. Theorem 106.14 — GCIC_G guaranteeDependent Subtyping, Refinement, and Graduality
  1382. Proposition 106.15 — Round trips at the list/vector boundaryDependent Subtyping, Refinement, and Graduality
  1383. Proposition 107.3 — Collapse under a bad boundDependent Object Types: Type Members, Bad Bounds, and Recursive Self
  1384. Lemma 107.6 — Tight-to-invertible bridgeDependent Object Types: Type Members, Bad Bounds, and Recursive Self
  1385. Lemma 107.7 — Selection replacementDependent Object Types: Type Members, Bad Bounds, and Recursive Self
  1386. Theorem 107.8 — General typing becomes tight in an inert contextDependent Object Types: Type Members, Bad Bounds, and Recursive Self
  1387. Theorem 107.9 — Canonical forms in inert contextsDependent Object Types: Type Members, Bad Bounds, and Recursive Self
  1388. Theorem 107.10 — Structural and safety theorem for simple DOTDependent Object Types: Type Members, Bad Bounds, and Recursive Self
  1389. Proposition 108.4 — Indexed replacement yields subtypingFully Path-Dependent Types: Stable Paths, Singletons, and Modules
  1390. Lemma 108.5 — Replacement preserves formationFully Path-Dependent Types: Stable Paths, Singletons, and Modules
  1391. Proposition 108.6 — Root formation does not form a changed leafFully Path-Dependent Types: Stable Paths, Singletons, and Modules
  1392. Proposition 108.8 — The body premise checks the installed receiverFully Path-Dependent Types: Stable Paths, Singletons, and Modules
  1393. Lemma 108.9 — Typed function paths terminate in lambdasFully Path-Dependent Types: Stable Paths, Singletons, and Modules
  1394. Theorem 108.10 — pDOT type safetyFully Path-Dependent Types: Stable Paths, Singletons, and Modules
  1395. Proposition 109.2 — Unrestricted-control counterexampleClassical Dependent Type Theory and Control
  1396. Lemma 109.5 — Dependent-context substitutionClassical Dependent Type Theory and Control
  1397. Theorem 109.6 — Subject reductionClassical Dependent Type Theory and Control
  1398. Lemma 109.9 — Linearity of the translation of NEF proofsClassical Dependent Type Theory and Control
  1399. Lemma 109.10 — Dependent CPS type for NEF proofsClassical Dependent Type Theory and Control
  1400. Theorem 109.11 — CPS type preservationClassical Dependent Type Theory and Control
  1401. Theorem 109.12 — Normalization and consistencyClassical Dependent Type Theory and Control
  1402. Proposition 109.13 — Boundary of the classical dependent principleClassical Dependent Type Theory and Control
  1403. Lemma 48.6 — Effective enumeration of derivationsTrusted Kernels and Bidirectional Checking
  1404. Proposition 48.9Trusted Kernels and Bidirectional Checking
  1405. Proposition 110.17 — Exact rule delta from the proof fragment to TimplTrusted Kernels and Bidirectional Checking
  1406. Proposition 48.17 — Determinism and terminationTrusted Kernels and Bidirectional Checking
  1407. Theorem 110.23 — Recheck soundness and round tripTrusted Kernels and Bidirectional Checking
  1408. Corollary 110.24 — Kernel guaranteeTrusted Kernels and Bidirectional Checking
  1409. Lemma 110.26 — Formation generation for TimplTrusted Kernels and Bidirectional Checking
  1410. Theorem 48.19 — SoundnessTrusted Kernels and Bidirectional Checking
  1411. Theorem 48.20 — Completeness up to annotationTrusted Kernels and Bidirectional Checking
  1412. Proposition 110.30 — Exact comparison boundaryTrusted Kernels and Bidirectional Checking
  1413. Theorem 48.40 — ETT lacks injective Π -typesTrusted Kernels and Bidirectional Checking
  1414. Theorem 48.47 — Undecidability of extensional equalityTrusted Kernels and Bidirectional Checking
  1415. Corollary 48.48Trusted Kernels and Bidirectional Checking
  1416. Proposition 49.3Canonicity, Normalization, and Decidable Conversion
  1417. Lemma 49.11 — Weakening and substitution for (-)^Canonicity, Normalization, and Decidable Conversion
  1418. Lemma 49.12 — Fundamental lemma of computabilityCanonicity, Normalization, and Decidable Conversion
  1419. Theorem 49.2 — Boolean canonicity for the elementary fragmentCanonicity, Normalization, and Decidable Conversion
  1420. Lemma 111.19 — Deciding level equality and level orderCanonicity, Normalization, and Decidable Conversion
  1421. Lemma 111.23 — Substitution, weakening, and conversion for reductionCanonicity, Normalization, and Decidable Conversion
  1422. Lemma 111.26 — Stability of the four judgmentsCanonicity, Normalization, and Decidable Conversion
  1423. Lemma 49.27 — RestrictionCanonicity, Normalization, and Decidable Conversion
  1424. Lemma 49.28 — Evaluation and substitutionCanonicity, Normalization, and Decidable Conversion
  1425. Theorem 49.29 — Completeness of NbE forCanonicity, Normalization, and Decidable Conversion
  1426. Lemma 49.31 — AdequacyCanonicity, Normalization, and Decidable Conversion
  1427. Lemma 49.32 — Fundamental lemma forCanonicity, Normalization, and Decidable Conversion
  1428. Theorem 49.33 — Soundness of NbE forCanonicity, Normalization, and Decidable Conversion
  1429. Corollary 49.34Canonicity, Normalization, and Decidable Conversion
  1430. Lemma 111.48 — Substitution and renaming equivarianceCanonicity, Normalization, and Decidable Conversion
  1431. Lemma 111.54 — Neutral relatedness is a partial equivalence relationCanonicity, Normalization, and Decidable Conversion
  1432. Lemma 111.55 — World-indexed neutral formationCanonicity, Normalization, and Decidable Conversion
  1433. Lemma 111.56 — World equivariance of neutral relatednessCanonicity, Normalization, and Decidable Conversion
  1434. Lemma 111.62 — The relations are functional partial equivalencesCanonicity, Normalization, and Decidable Conversion
  1435. Lemma 111.63 — Reification is determined by relatednessCanonicity, Normalization, and Decidable Conversion
  1436. Lemma 111.64 — Substitution action on ranked semantic evidenceCanonicity, Normalization, and Decidable Conversion
  1437. Lemma 111.66 — Kripke evidence independenceCanonicity, Normalization, and Decidable Conversion
  1438. Lemma 111.69 — Escape, reflection, world stability, and quotation normalityCanonicity, Normalization, and Decidable Conversion
  1439. Lemma 111.70 — Quotation lands in normal syntaxCanonicity, Normalization, and Decidable Conversion
  1440. Lemma 111.72 — Evaluation, weakening, and substitutionCanonicity, Normalization, and Decidable Conversion
  1441. Lemma 111.73 — Semantic liftingCanonicity, Normalization, and Decidable Conversion
  1442. Lemma 111.74 — Fundamental lemma for T_ implCanonicity, Normalization, and Decidable Conversion
  1443. Lemma 111.75 — The identity environment is validCanonicity, Normalization, and Decidable Conversion
  1444. Theorem 111.76 — Normalization for T_ implCanonicity, Normalization, and Decidable Conversion
  1445. Lemma 111.77 — StabilityCanonicity, Normalization, and Decidable Conversion
  1446. Theorem 49.18 — Canonicity and canonical formsCanonicity, Normalization, and Decidable Conversion
  1447. Corollary 49.20 — DecidabilityCanonicity, Normalization, and Decidable Conversion
  1448. Theorem 111.81 — The Timpl conversion interfaceCanonicity, Normalization, and Decidable Conversion
  1449. Corollary 111.82 — The kernel is unconditionalCanonicity, Normalization, and Decidable Conversion
  1450. Theorem 49.17 — NormalizationCanonicity, Normalization, and Decidable Conversion
  1451. Lemma 112.8 — Generation invariantElaboration and Unification
  1452. Lemma 112.10 — Exact level normalizationElaboration and Unification
  1453. Theorem 112.13 — Canonical stratified level solutionElaboration and Unification
  1454. Lemma 112.16 — Rigid simplification preserves solutionsElaboration and Unification
  1455. Lemma 112.19 — Flex–rigid most generalityElaboration and Unification
  1456. Lemma 112.21 — Contextual factorizationElaboration and Unification
  1457. Lemma 112.22 — Common-support factorizationElaboration and Unification
  1458. Lemma 112.23 — Flex–flex most generalityElaboration and Unification
  1459. Theorem 112.24 — Terminating pattern simplificationElaboration and Unification
  1460. Theorem 112.26 — Constraint-generation soundnessElaboration and Unification
  1461. Lemma 112.28 — Timpl certificate completionElaboration and Unification
  1462. Corollary 112.29 — Elaboration soundnessElaboration and Unification
  1463. Theorem 112.32 — Completeness for the decidable policyElaboration and Unification
  1464. Theorem 112.36 — Reed simplification: exact boundaryElaboration and Unification
  1465. Proposition 112.40 — Soundness and erasure of the source elaboratorElaboration and Unification
  1466. Lemma 113.3 — Valid-congruence criterionEfficient First-Order Unification
  1467. Lemma 113.5 — Root transition and closure invariantEfficient First-Order Unification
  1468. Theorem 113.6 — Termination, correctness, and compact MGUEfficient First-Order Unification
  1469. Lemma 113.8 — Scheduling refinementEfficient First-Order Unification
  1470. Theorem 113.9 — Linear pointer-machine implementationEfficient First-Order Unification
  1471. Proposition 113.10 — Placement of the completion markEfficient First-Order Unification
  1472. Proposition 113.11 — Expansion is outside the linear boundEfficient First-Order Unification
  1473. Lemma 114.3 — Primitive validityProof-Producing Tactics and the Kernel Boundary
  1474. Theorem 114.5 — Tactic soundnessProof-Producing Tactics and the Kernel Boundary
  1475. Proposition 114.7 — Closure removes tactic stateProof-Producing Tactics and the Kernel Boundary
  1476. Theorem 114.10 — Kernel-boundary theoremProof-Producing Tactics and the Kernel Boundary
  1477. Theorem 115.4 — Simplifier preservationRewriting, Simplification, and Reflection
  1478. Proposition 115.7 — Contextual preservationRewriting, Simplification, and Reflection
  1479. Lemma 115.9 — Evaluation of multiplicity normal formsRewriting, Simplification, and Reflection
  1480. Theorem 115.10 — Reflection checker soundnessRewriting, Simplification, and Reflection
  1481. Theorem 116.5 — No accidental captureTyped Metaprogramming and Hygienic Elaboration
  1482. Lemma 116.8 — Phase-indexed substitutionTyped Metaprogramming and Hygienic Elaboration
  1483. Theorem 116.10 — Mutual typing and provenance of macro-free expansionTyped Metaprogramming and Hygienic Elaboration
  1484. Corollary 116.13 — Generated declarations preserve kernel trustTyped Metaprogramming and Hygienic Elaboration
  1485. Theorem 116.15 — Soundness of λ ^Typed Metaprogramming and Hygienic Elaboration
  1486. Proposition 117.4 — Lift is an isomorphism on termsFirst-Class Universe Levels and Level Polymorphism
  1487. Lemma 117.6 — Level substitutionFirst-Class Universe Levels and Level Polymorphism
  1488. Lemma 117.8 — Level normalization is soundFirst-Class Universe Levels and Level Polymorphism
  1489. Lemma 117.9 — Level normalization is completeFirst-Class Universe Levels and Level Polymorphism
  1490. Corollary 117.10 — Level equality is decidableFirst-Class Universe Levels and Level Polymorphism
  1491. Theorem 117.11 — Metatheory of the principal systemFirst-Class Universe Levels and Level Polymorphism
  1492. Lemma 118.4 — Elimination stability under instantiationSort Polymorphism and Stratified Type Theory
  1493. Proposition 118.6 — Solutions are checkable and finitely manySort Polymorphism and Stratified Type Theory
  1494. Theorem 118.8 — Monomorphization theoremSort Polymorphism and Stratified Type Theory
  1495. Corollary 118.9 — EquiconsistencySort Polymorphism and Stratified Type Theory
  1496. Theorem 118.10 — Imported λ * inconsistencySort Polymorphism and Stratified Type Theory
  1497. Theorem 118.13 — Bounded-sort packageSort Polymorphism and Stratified Type Theory
  1498. Lemma 119.3 — Structural stability of coercion pathsCoercive Subtyping and Coherent Cast Insertion
  1499. Theorem 119.7 — Elaboration type preservationCoercive Subtyping and Coherent Cast Insertion
  1500. Lemma 119.8 — Synthesis is determinedCoercive Subtyping and Coherent Cast Insertion
  1501. Theorem 119.9 — Coherence of insertionCoercive Subtyping and Coherent Cast Insertion
  1502. Proposition 119.10 — Coherence of the dependent function castCoercive Subtyping and Coherent Cast Insertion
  1503. Theorem 119.11 — Completion and conservativity at the source signatureCoercive Subtyping and Coherent Cast Insertion
  1504. Proposition 120.4 — Constructor functor laws for descriptionsDefinitional Functoriality and Generic Type-Former Action
  1505. Theorem 120.6 — Extended definitional functor laws for descriptionsDefinitional Functoriality and Generic Type-Former Action
  1506. Lemma 120.8 — Product and sum functor lawsDefinitional Functoriality and Generic Type-Former Action
  1507. Lemma 120.11 — Uniqueness of weak-head selectionDefinitional Functoriality and Generic Type-Former Action
  1508. Lemma 120.12 — Typed-context preservationDefinitional Functoriality and Generic Type-Former Action
  1509. Lemma 120.13 — Generated action commutes with substitutionDefinitional Functoriality and Generic Type-Former Action
  1510. Lemma 120.14 — Primitive actions commute with substitutionDefinitional Functoriality and Generic Type-Former Action
  1511. Proposition 120.15 — Compaction is an instance of the composition lawDefinitional Functoriality and Generic Type-Former Action
  1512. Theorem 120.16 — Metatheory of MLTT_Definitional Functoriality and Generic Type-Former Action
  1513. Lemma 120.17 — Local uniqueness of typingDefinitional Functoriality and Generic Type-Former Action
  1514. Theorem 120.18 — Typing preservation for the functoriality deltaDefinitional Functoriality and Generic Type-Former Action
  1515. Proposition 120.20 — AdapTT semantic boundaryDefinitional Functoriality and Generic Type-Former Action
  1516. Lemma 121.4 — Matching decomposition preserves the least rowCompiling Dependent Pattern Matching
  1517. Lemma 121.13 — Termination of matrix compilation, relative formCompiling Dependent Pattern Matching
  1518. Lemma 121.14 — Specialization preserves the row-map invariantCompiling Dependent Pattern Matching
  1519. Lemma 121.15 — Selected-row factorizationCompiling Dependent Pattern Matching
  1520. Lemma 121.16 — Recursive-leaf replacement through BelowCompiling Dependent Pattern Matching
  1521. Theorem 121.17 — Compilation typingCompiling Dependent Pattern Matching
  1522. Theorem 121.18 — Case-tree-to-eliminator loweringCompiling Dependent Pattern Matching
  1523. Theorem 121.19 — First-match simulation and failure witnessesCompiling Dependent Pattern Matching
  1524. Corollary 121.20 — Selected-clause compositionCompiling Dependent Pattern Matching
  1525. Proposition 121.21 — Equation generation is exactCompiling Dependent Pattern Matching
  1526. Lemma 121.22 — One-step closed simulation after administrative beta reductionCompiling Dependent Pattern Matching
  1527. Theorem 121.23 — Target evaluation reproduces source evaluationCompiling Dependent Pattern Matching
  1528. Lemma 122.6 — Datatype rejection records a failed premiseDatatype Declaration Blocks and Strict Positivity
  1529. Lemma 122.7 — A nonpositive state is family-freeDatatype Declaration Blocks and Strict Positivity
  1530. Lemma 122.10 — Termination of the declaration checkerDatatype Declaration Blocks and Strict Positivity
  1531. Lemma 122.11 — Accepted blocks are strictly positiveDatatype Declaration Blocks and Strict Positivity
  1532. Lemma 122.14 — Every accepted binder yields a hypothesisDatatype Declaration Blocks and Strict Positivity
  1533. Theorem 122.15 — Generated-rule well-formednessDatatype Declaration Blocks and Strict Positivity
  1534. Theorem 122.16 — Timpl-data elaboration soundnessDatatype Declaration Blocks and Strict Positivity
  1535. Lemma 123.6 — Recursive rejection records a failed predecessor premiseRecursive Function Groups and Termination
  1536. Lemma 123.8 — Inverse images preserve well-foundednessRecursive Function Groups and Termination
  1537. Lemma 123.9 — Finite lexicographic products are well foundedRecursive Function Groups and Termination
  1538. Lemma 123.11 — A stored structural certificate gives its discipline's child stepRecursive Function Groups and Termination
  1539. Lemma 123.12 — The accepted call relation is well foundedRecursive Function Groups and Termination
  1540. Lemma 123.14 — Body translation is typedRecursive Function Groups and Termination
  1541. Lemma 123.16 — Generated equationsRecursive Function Groups and Termination
  1542. Lemma 123.17 — One-step operational correspondenceRecursive Function Groups and Termination
  1543. Lemma 123.18 — Finite operational correspondenceRecursive Function Groups and Termination
  1544. Theorem 123.19 — Termination and elaboration of accepted groupsRecursive Function Groups and Termination
  1545. Corollary 123.20 — Functional induction for an accepted groupRecursive Function Groups and Termination
  1546. Lemma 124.3 — Group-free normalization and evaluation interfaceCorecursive Definitions, Copatterns, and Productivity
  1547. Lemma 124.4 — Preparation is total and uniqueCorecursive Definitions, Copatterns, and Productivity
  1548. Lemma 124.8 — Guard checking terminatesCorecursive Definitions, Copatterns, and Productivity
  1549. Lemma 124.9 — One demanded destructor makes progressCorecursive Definitions, Copatterns, and Productivity
  1550. Theorem 124.10 — Productivity of accepted stream groupsCorecursive Definitions, Copatterns, and Productivity
  1551. Lemma 124.12 — Preparation composes with group-free substitutionCorecursive Definitions, Copatterns, and Productivity
  1552. Lemma 124.13 — Prepared tuples are fixed pointsCorecursive Definitions, Copatterns, and Productivity
  1553. Lemma 124.14 — Source/map evaluation agreementCorecursive Definitions, Copatterns, and Productivity
  1554. Theorem 124.15 — Finite-observation simulationCorecursive Definitions, Copatterns, and Productivity
  1555. Lemma 125.6 — Frontier substitutionElaborating Dependent Copattern Definitions
  1556. Theorem 125.7 — Clause-to-case-tree typingElaborating Dependent Copattern Definitions
  1557. Lemma 125.8 — Source and case-tree observations agreeElaborating Dependent Copattern Definitions
  1558. Lemma 125.11 — Generated state-block formationElaborating Dependent Copattern Definitions
  1559. Lemma 125.13 — Coprojection method typingElaborating Dependent Copattern Definitions
  1560. Theorem 125.14 — Case-tree-to-core typingElaborating Dependent Copattern Definitions
  1561. Lemma 125.16 — Compiled application preparation is total and functionalElaborating Dependent Copattern Definitions
  1562. Lemma 125.18 — Case-tree and core observations agreeElaborating Dependent Copattern Definitions
  1563. Theorem 125.19 — Composed elaboration and observation preservationElaborating Dependent Copattern Definitions
  1564. Lemma 126.2 — Texec values and evaluation are functionalErasure and Execution of Dependent Definitions
  1565. Lemma 126.4 — Relevance is stable under marked substitutionErasure and Execution of Dependent Definitions
  1566. Lemma 126.6 — Source evaluation is sound for judgmental equalityErasure and Execution of Dependent Definitions
  1567. Lemma 126.7 — Source evaluation preserves typingErasure and Execution of Dependent Definitions
  1568. Lemma 126.8 — Source evaluation preserves runtime relevanceErasure and Execution of Dependent Definitions
  1569. Lemma 126.11 — Relevance and erasure under substitutionErasure and Execution of Dependent Definitions
  1570. Lemma 126.13 — Erasure produces well-formed target syntaxErasure and Execution of Dependent Definitions
  1571. Theorem 126.14 — Forward execution simulationErasure and Execution of Dependent Definitions
  1572. Lemma 126.16 — Target observation is functionalErasure and Execution of Dependent Definitions
  1573. Lemma 126.17 — First-order source and normalizer agreementErasure and Execution of Dependent Definitions
  1574. Lemma 126.18 — Generated-map evaluation agreementErasure and Execution of Dependent Definitions
  1575. Theorem 126.19 — Coiterator erasure simulationErasure and Execution of Dependent Definitions
  1576. Corollary 126.20 — Accepted stream-call erasureErasure and Execution of Dependent Definitions
  1577. Theorem 126.22 — System Fi index-erasure interfaceErasure and Execution of Dependent Definitions
  1578. Corollary 126.23 — Normalization and consistency of System FiErasure and Execution of Dependent Definitions
  1579. Lemma 127.3 — Residual variablesPartial Evaluation, Binding-Time Analysis, and the Futamura Projections
  1580. Theorem 127.4 — Online specialization equationPartial Evaluation, Binding-Time Analysis, and the Futamura Projections
  1581. Lemma 127.7 — Memo completion and finite simulationPartial Evaluation, Binding-Time Analysis, and the Futamura Projections
  1582. Lemma 127.8 — Residual-program monotonicityPartial Evaluation, Binding-Time Analysis, and the Futamura Projections
  1583. Theorem 127.9 — Safe-fuel search termination and preservationPartial Evaluation, Binding-Time Analysis, and the Futamura Projections
  1584. Lemma 127.10 — Evaluation decomposition for substitutionPartial Evaluation, Binding-Time Analysis, and the Futamura Projections
  1585. Proposition 127.11 — Let-insertion preservationPartial Evaluation, Binding-Time Analysis, and the Futamura Projections
  1586. Lemma 127.13 — Binding-time consistencyPartial Evaluation, Binding-Time Analysis, and the Futamura Projections
  1587. Lemma 127.14 — Completed-graph node simulationPartial Evaluation, Binding-Time Analysis, and the Futamura Projections
  1588. Theorem 127.15 — Well-annotated-program soundnessPartial Evaluation, Binding-Time Analysis, and the Futamura Projections
  1589. Proposition 127.16 — Binding-time split preservationPartial Evaluation, Binding-Time Analysis, and the Futamura Projections
  1590. Proposition 127.17 — Scheme0 self-application typing boundaryPartial Evaluation, Binding-Time Analysis, and the Futamura Projections
  1591. Theorem 127.18 — The three Futamura equationsPartial Evaluation, Binding-Time Analysis, and the Futamura Projections
  1592. Lemma 127.19 — Finite binding-time analysisPartial Evaluation, Binding-Time Analysis, and the Futamura Projections
  1593. Theorem 128.2 — Local driving coverageSupercompilation, Driving, and Generalization
  1594. Lemma 128.3 — Folding equationSupercompilation, Driving, and Generalization
  1595. Theorem 128.4 — Whistle propertySupercompilation, Driving, and Generalization
  1596. Lemma 128.5 — Generalization witnessesSupercompilation, Driving, and Generalization
  1597. Lemma 128.7 — Local strong-improvement lawsSupercompilation, Driving, and Generalization
  1598. Lemma 128.8 — Local recursive replacementSupercompilation, Driving, and Generalization
  1599. Lemma 128.9 — Allocation and call bridgeSupercompilation, Driving, and Generalization
  1600. Lemma 128.10 — Clause adequacy for the full driverSupercompilation, Driving, and Generalization
  1601. Lemma 128.12 — Ledger totality and functionalitySupercompilation, Driving, and Generalization
  1602. Lemma 128.13 — Strict descent of recursive driver callsSupercompilation, Driving, and Generalization
  1603. Theorem 128.14 — SC-CBV termination and correctnessSupercompilation, Driving, and Generalization
  1604. Proposition 128.16 — Residual well-scopednessSupercompilation, Driving, and Generalization
  1605. Lemma 129.1 — Dual substitutionTyped Multi-Stage Programming and an Evidence-Bounded Interpreter-Tower Case Study
  1606. Theorem 129.2 — Local eliminability and inert-label persistenceTyped Multi-Stage Programming and an Evidence-Bounded Interpreter-Tower Case Study
  1607. Theorem 129.3 — Subject reduction and scope safetyTyped Multi-Stage Programming and an Evidence-Bounded Interpreter-Tower Case Study
  1608. Theorem 129.4 — Two-level embeddingTyped Multi-Stage Programming and an Evidence-Bounded Interpreter-Tower Case Study
  1609. Proposition 129.5 — Type preservation for the Scheme0 arithmetic bridgeTyped Multi-Stage Programming and an Evidence-Bounded Interpreter-Tower Case Study
  1610. Lemma 129.6 — Arithmetic specialization for both binding timesTyped Multi-Stage Programming and an Evidence-Bounded Interpreter-Tower Case Study
  1611. Proposition 129.7 — Annotated arithmetic commuting instanceTyped Multi-Stage Programming and an Evidence-Bounded Interpreter-Tower Case Study
  1612. Proposition 129.8 — Pure tagless-final representationTyped Multi-Stage Programming and an Evidence-Bounded Interpreter-Tower Case Study
  1613. Proposition 129.9 — Pure tagless-final partial-evaluation equationTyped Multi-Stage Programming and an Evidence-Bounded Interpreter-Tower Case Study
  1614. Theorem 129.10 — MacoCaml elaboration soundnessTyped Multi-Stage Programming and an Evidence-Bounded Interpreter-Tower Case Study
  1615. Lemma 129.11 — Tan–Wei logical-relation interfaceTyped Multi-Stage Programming and an Evidence-Bounded Interpreter-Tower Case Study
  1616. Theorem 129.12 — Source-bounded staging-erasure equivalenceTyped Multi-Stage Programming and an Evidence-Bounded Interpreter-Tower Case Study
  1617. Lemma 130.1 — Code-head inversion for type equivalenceDependent Multi-Stage Type Theory
  1618. Lemma 130.2 — Quotation and escape inversionDependent Multi-Stage Type Theory
  1619. Lemma 130.3 — Simultaneous structural and substitution packageDependent Multi-Stage Type Theory
  1620. Proposition 130.4 — Dependent annotations obstruct exact confluenceDependent Multi-Stage Type Theory
  1621. Theorem 130.5 — PreservationDependent Multi-Stage Type Theory
  1622. Lemma 130.6 — Simple erasure and full-step simulationDependent Multi-Stage Type Theory
  1623. Theorem 130.7 — Strong normalization of full reductionDependent Multi-Stage Type Theory
  1624. Lemma 130.8 — Substitution compatibility of word-parallel reductionDependent Multi-Stage Type Theory
  1625. Lemma 130.9 — Word-parallel diamondDependent Multi-Stage Type Theory
  1626. Proposition 130.10 — Confluence of annotation-free reductionDependent Multi-Stage Type Theory
  1627. Theorem 130.11 — Confluence modulo binder annotationsDependent Multi-Stage Type Theory
  1628. Corollary 130.12 — Unique full normal forms modulo annotationsDependent Multi-Stage Type Theory
  1629. Lemma 130.13 — Type-constructor head separationDependent Multi-Stage Type Theory
  1630. Lemma 130.14 — Empty-stage value headsDependent Multi-Stage Type Theory
  1631. Theorem 130.15 — Unique staged decompositionDependent Multi-Stage Type Theory
  1632. Corollary 130.16 — Staged progress and type safetyDependent Multi-Stage Type Theory
  1633. Lemma 131.4 — Kind uniquenessExplicit Equality Evidence and System FC
  1634. Lemma 131.5 — WeakeningExplicit Equality Evidence and System FC
  1635. Lemma 131.11 — ReflexivityExplicit Equality Evidence and System FC
  1636. Theorem 131.12 — LiftingExplicit Equality Evidence and System FC
  1637. Proposition 131.16 — Failure of regularity for the printed decomposition rulesExplicit Equality Evidence and System FC
  1638. Lemma 131.18 — Kinding substitutionExplicit Equality Evidence and System FC
  1639. Theorem 131.19 — Coercion regularityExplicit Equality Evidence and System FC
  1640. Lemma 131.25 — Term substitutionExplicit Equality Evidence and System FC
  1641. Lemma 131.26 — Type and coercion substitution in termsExplicit Equality Evidence and System FC
  1642. Theorem 131.27 — PreservationExplicit Equality Evidence and System FC
  1643. Lemma 131.30 — Canonical formsExplicit Equality Evidence and System FC
  1644. Theorem 131.31 — Progress and subject reductionExplicit Equality Evidence and System FC
  1645. Corollary 131.32 — Syntactic soundnessExplicit Equality Evidence and System FC
  1646. Theorem 131.35 — ErasureExplicit Equality Evidence and System FC
  1647. Corollary 131.36 — Erasure soundnessExplicit Equality Evidence and System FC
  1648. Lemma 131.40 — Elaboration is type preservingExplicit Equality Evidence and System FC
  1649. Theorem 131.41 — GADT consistencyExplicit Equality Evidence and System FC
  1650. Lemma 132.6 — Regularity of definitional equalitySystems D and DC: A Dependent Haskell Core Specification
  1651. Lemma 132.9 — SubstitutivitySystems D and DC: A Dependent Haskell Core Specification
  1652. Lemma 132.10 — Inversion for abstractionSystems D and DC: A Dependent Haskell Core Specification
  1653. Theorem 132.11 — PreservationSystems D and DC: A Dependent Haskell Core Specification
  1654. Theorem 132.14 — Confluence of parallel reduction; importedSystems D and DC: A Dependent Haskell Core Specification
  1655. Theorem 132.15 — Equality implies joinabilitySystems D and DC: A Dependent Haskell Core Specification
  1656. Theorem 132.16 — Joinability implies consistencySystems D and DC: A Dependent Haskell Core Specification
  1657. Corollary 132.17 — Consistency for DSystems D and DC: A Dependent Haskell Core Specification
  1658. Theorem 132.19 — ProgressSystems D and DC: A Dependent Haskell Core Specification
  1659. Lemma 132.24 — Coercion regularity for DCSystems D and DC: A Dependent Haskell Core Specification
  1660. Lemma 132.25 — Decidability and uniquenessSystems D and DC: A Dependent Haskell Core Specification
  1661. Lemma 132.27 — Erasure and annotationSystems D and DC: A Dependent Haskell Core Specification
  1662. Lemma 132.28 — Reduction erasureSystems D and DC: A Dependent Haskell Core Specification
  1663. Corollary 132.29 — Annotations do not change behaviourSystems D and DC: A Dependent Haskell Core Specification
  1664. Lemma 133.4 — CPS type correctnessTyped Intermediate Languages and Certified Closure Conversion
  1665. Lemma 133.7 — Closure conversion type correctnessTyped Intermediate Languages and Certified Closure Conversion
  1666. Lemma 133.8 — HoistingTyped Intermediate Languages and Certified Closure Conversion
  1667. Lemma 133.11 — Allocation type correctnessTyped Intermediate Languages and Certified Closure Conversion
  1668. Theorem 133.13 — Subject reduction and progressTyped Intermediate Languages and Certified Closure Conversion
  1669. Corollary 133.14 — Type safetyTyped Intermediate Languages and Certified Closure Conversion
  1670. Lemma 133.15 — Code generationTyped Intermediate Languages and Certified Closure Conversion
  1671. Corollary 133.16 — Compiler type correctnessTyped Intermediate Languages and Certified Closure Conversion
  1672. Proposition 133.17 — Type preservation does not imply semantic preservationTyped Intermediate Languages and Certified Closure Conversion
  1673. Lemma 133.19 — Linking preserves typingTyped Intermediate Languages and Certified Closure Conversion
  1674. Proposition 134.2 — Type preservation has no content hereA Certified Type-Preserving Compiler to Assembly
  1675. Lemma 134.6 — Splicing is soundA Certified Type-Preserving Compiler to Assembly
  1676. Theorem 134.7 — Linearization is soundA Certified Type-Preserving Compiler to Assembly
  1677. Lemma 134.8 — Weakening is denotation-preservingA Certified Type-Preserving Compiler to Assembly
  1678. Theorem 134.15 — Closure conversion is soundA Certified Type-Preserving Compiler to Assembly
  1679. Theorem 134.17 — Heap rearrangement safetyA Certified Type-Preserving Compiler to Assembly
  1680. Theorem 134.18 — Compiler correctnessA Certified Type-Preserving Compiler to Assembly
  1681. Proposition 135.3 — Closure conversion is correctDefunctionalization, Refunctionalization, and Abstract Machines
  1682. Proposition 135.5 — The transformation is correctDefunctionalization, Refunctionalization, and Abstract Machines
  1683. Proposition 135.7 — Defunctionalization is correctDefunctionalization, Refunctionalization, and Abstract Machines
  1684. Theorem 135.9 — The derived machine is Krivine'sDefunctionalization, Refunctionalization, and Abstract Machines
  1685. Proposition 135.12 — The condition is not automaticDefunctionalization, Refunctionalization, and Abstract Machines
  1686. Theorem 135.15 — Round tripDefunctionalization, Refunctionalization, and Abstract Machines
  1687. Theorem 136.5 — RTP and RTC are equivalentSecure Compilation and Robust Property Preservation
  1688. Theorem 136.8 — Both characterizations are equivalent to their criteriaSecure Compilation and Robust Property Preservation
  1689. Theorem 136.9 — DecompositionSecure Compilation and Robust Property Preservation
  1690. Theorem 136.11Secure Compilation and Robust Property Preservation
  1691. Theorem 136.14 — Full abstraction does not imply robust safety preservationSecure Compilation and Robust Property Preservation
  1692. Theorem 136.15 — A converse, under hypotheses; importedSecure Compilation and Robust Property Preservation
  1693. Proposition 137.4 — The existential encoding needs impredicativityDependent Closure Conversion for the Calculus of Constructions
  1694. Lemma 137.10 — The closure's type reduces to the translated typeDependent Closure Conversion for the Calculus of Constructions
  1695. Lemma 137.12 — CompositionalityDependent Closure Conversion for the Calculus of Constructions
  1696. Lemma 137.13 — Preservation of reductionDependent Closure Conversion for the Calculus of Constructions
  1697. Lemma 137.14 — CoherenceDependent Closure Conversion for the Calculus of Constructions
  1698. Theorem 137.15 — Type preservationDependent Closure Conversion for the Calculus of Constructions
  1699. Lemma 137.17Dependent Closure Conversion for the Calculus of Constructions
  1700. Theorem 137.18 — Consistency and type safety of CC-CCDependent Closure Conversion for the Calculus of Constructions
  1701. Theorem 137.21 — Correctness of separate compilationDependent Closure Conversion for the Calculus of Constructions
  1702. Corollary 137.22 — Whole-program correctnessDependent Closure Conversion for the Calculus of Constructions
  1703. Lemma 138.9 — Continuation cutDependency-Preserving A-Normal Form
  1704. Lemma 138.10 — Continuation cut modulo equivalenceDependency-Preserving A-Normal Form
  1705. Theorem 138.13 — The output is in A-normal formDependency-Preserving A-Normal Form
  1706. Lemma 138.15 — Type preservation, strengthenedDependency-Preserving A-Normal Form
  1707. Theorem 138.16 — Type preservationDependency-Preserving A-Normal Form
  1708. Lemma 138.17 — Compositionality and substitutionDependency-Preserving A-Normal Form
  1709. Lemma 138.19Dependency-Preserving A-Normal Form
  1710. Theorem 138.20 — Consistency and subject reductionDependency-Preserving A-Normal Form
  1711. Theorem 138.21 — Evaluation soundnessDependency-Preserving A-Normal Form
  1712. Theorem 138.22 — Correctness of separate compilationDependency-Preserving A-Normal Form
  1713. Proposition 138.23 — The translation duplicates codeDependency-Preserving A-Normal Form
  1714. Lemma 138.25 — The join-point translation is type preservingDependency-Preserving A-Normal Form
  1715. Proposition 139.7 — Substitution preserves semanticsTyped Functional Array Languages: Shapes, Uniqueness, and Parallel Compilation
  1716. Proposition 139.12 — ExtensibilityTyped Functional Array Languages: Shapes, Uniqueness, and Parallel Compilation
  1717. Proposition 139.13 — Dynamic size matching and checkingTyped Functional Array Languages: Shapes, Uniqueness, and Parallel Compilation
  1718. Proposition 139.14 — Value subtypingTyped Functional Array Languages: Shapes, Uniqueness, and Parallel Compilation
  1719. Theorem 139.15 — SoundnessTyped Functional Array Languages: Shapes, Uniqueness, and Parallel Compilation
  1720. Theorem 140.4 — Parallel substitution; importedVerified Metatheory and Realistic Trusted Kernels
  1721. Theorem 140.5 — Triangle property; importedVerified Metatheory and Realistic Trusted Kernels
  1722. Corollary 140.6 — One-step diamondVerified Metatheory and Realistic Trusted Kernels
  1723. Lemma 140.7 — Diamond closureVerified Metatheory and Realistic Trusted Kernels
  1724. Corollary 140.8 — Confluence of parallel reductionVerified Metatheory and Realistic Trusted Kernels
  1725. Theorem 140.14 — Soundness of the checkerVerified Metatheory and Realistic Trusted Kernels
  1726. Proposition 140.19 — The function does not commute with evaluationVerified Metatheory and Realistic Trusted Kernels
  1727. Lemma 140.21 — Structural erasure lemmasVerified Metatheory and Realistic Trusted Kernels
  1728. Theorem 140.22 — Erasure correctnessVerified Metatheory and Realistic Trusted Kernels
  1729. Proposition 140.23 — Where the function and the relation agreeVerified Metatheory and Realistic Trusted Kernels
  1730. Lemma 141.2 — Trivial substitutionsCategories, Functors, and Representability
  1731. Lemma 141.3 — Action preserves typingCategories, Functors, and Representability
  1732. Lemma 141.5 — Action lawCategories, Functors, and Representability
  1733. Proposition 141.7 — The substitution algebraCategories, Functors, and Representability
  1734. Proposition 141.11 — One-object categoriesCategories, Functors, and Representability
  1735. Lemma 141.22 — Inverses are uniqueCategories, Functors, and Representability
  1736. Lemma 141.27 — Uniqueness up to isomorphismCategories, Functors, and Representability
  1737. Proposition 141.29 — Cancellation inCategories, Functors, and Representability
  1738. Proposition 141.31 — Monic and epic but not invertibleCategories, Functors, and Representability
  1739. Proposition 141.35 — Functors out of a free categoryCategories, Functors, and Representability
  1740. Proposition 141.36 — Environments form a functorCategories, Functors, and Representability
  1741. Proposition 141.37 — Hom-functorsCategories, Functors, and Representability
  1742. Proposition 141.39 — Terms form a presheafCategories, Functors, and Representability
  1743. Proposition 141.43 — Natural isomorphismsCategories, Functors, and Representability
  1744. Theorem 141.46 — Characterization of equivalencesCategories, Functors, and Representability
  1745. Lemma 141.47 — Inverse functors are unique up to natural isomorphismCategories, Functors, and Representability
  1746. Proposition 141.48 — Named and nameless contextsCategories, Functors, and Representability
  1747. Lemma 141.51 — PrecompositionCategories, Functors, and Representability
  1748. Theorem 141.52 — YonedaCategories, Functors, and Representability
  1749. Corollary 141.53 — Yoneda for presheavesCategories, Functors, and Representability
  1750. Proposition 141.55 — The hom bifunctorCategories, Functors, and Representability
  1751. Lemma 141.56 — Naturality in each variableCategories, Functors, and Representability
  1752. Proposition 141.57 — Yoneda as a natural isomorphismCategories, Functors, and Representability
  1753. Corollary 141.59 — The embedding is fully faithfulCategories, Functors, and Representability
  1754. Proposition 141.60 — Terms are represented by one variableCategories, Functors, and Representability
  1755. Theorem 141.61 — Natural operations on terms are substitutionsCategories, Functors, and Representability
  1756. Proposition 141.62 — Extension of a contextCategories, Functors, and Representability
  1757. Theorem 141.63 — Natural binary operations are two-variable termsCategories, Functors, and Representability
  1758. Proposition 141.65 — Representability by a terminal elementCategories, Functors, and Representability
  1759. Lemma 142.2 — Pairing calculusAdjunctions, Limits, and Locally Cartesian Closure
  1760. Lemma 142.3 — Uniqueness of productsAdjunctions, Limits, and Locally Cartesian Closure
  1761. Proposition 142.7 — Concatenation is the product of contextsAdjunctions, Limits, and Locally Cartesian Closure
  1762. Proposition 142.9 — The set-theoretic pullbackAdjunctions, Limits, and Locally Cartesian Closure
  1763. Proposition 142.11 — Context extension is a pullbackAdjunctions, Limits, and Locally Cartesian Closure
  1764. Theorem 142.15 — Finite limits from products and equalizersAdjunctions, Limits, and Locally Cartesian Closure
  1765. Corollary 142.16 — Pullbacks from products and equalizersAdjunctions, Limits, and Locally Cartesian Closure
  1766. Proposition 142.18 — The free monoid is left adjoint to the underlying setAdjunctions, Limits, and Locally Cartesian Closure
  1767. Theorem 142.21 — The two presentations agreeAdjunctions, Limits, and Locally Cartesian Closure
  1768. Theorem 142.23 — PreservationAdjunctions, Limits, and Locally Cartesian Closure
  1769. Corollary 142.24Adjunctions, Limits, and Locally Cartesian Closure
  1770. Proposition 142.27 — Currying is an adjunctionAdjunctions, Limits, and Locally Cartesian Closure
  1771. Proposition 142.30 — The syntactic category is cartesian closedAdjunctions, Limits, and Locally Cartesian Closure
  1772. Proposition 142.32 — Elementary structure of a sliceAdjunctions, Limits, and Locally Cartesian Closure
  1773. Theorem 142.34 — Dependent sum is left adjoint to substitutionAdjunctions, Limits, and Locally Cartesian Closure
  1774. Proposition 142.35 — Slices over a set are familiesAdjunctions, Limits, and Locally Cartesian Closure
  1775. Lemma 142.37 — Adjunctions composeAdjunctions, Limits, and Locally Cartesian Closure
  1776. Theorem 142.38 — Dependent products give local closureAdjunctions, Limits, and Locally Cartesian Closure
  1777. Proposition 142.39 — The three functors on familiesAdjunctions, Limits, and Locally Cartesian Closure
  1778. Proposition 142.41 — Weakening is the substitution functorAdjunctions, Limits, and Locally Cartesian Closure
  1779. Theorem 142.42 — The dependent product along a display mapAdjunctions, Limits, and Locally Cartesian Closure
  1780. Proposition 142.43 — The dependent sum along a display mapAdjunctions, Limits, and Locally Cartesian Closure
  1781. Proposition 143.4 — Inverse image is a homomorphismCategorical Logic, Hyperdoctrines, and Internal Languages
  1782. Theorem 143.5 — The powerset quantifiersCategorical Logic, Hyperdoctrines, and Internal Languages
  1783. Proposition 143.6 — Weakening is a right adjoint, hence preserves meetsCategorical Logic, Hyperdoctrines, and Internal Languages
  1784. Lemma 143.9 — Substitution squares are pullbacksCategorical Logic, Hyperdoctrines, and Internal Languages
  1785. Theorem 143.11 — Beck–Chevalley in the powersetCategorical Logic, Hyperdoctrines, and Internal Languages
  1786. Proposition 143.13 — FrobeniusCategorical Logic, Hyperdoctrines, and Internal Languages
  1787. Theorem 143.15 — Lawvere's lawCategorical Logic, Hyperdoctrines, and Internal Languages
  1788. Proposition 143.18 — The powerset hyperdoctrine has comprehensionCategorical Logic, Hyperdoctrines, and Internal Languages
  1789. Lemma 143.23 — SubstitutionCategorical Logic, Hyperdoctrines, and Internal Languages
  1790. Theorem 143.24 — SoundnessCategorical Logic, Hyperdoctrines, and Internal Languages
  1791. Proposition 143.25 — Frobenius from Beck–ChevalleyCategorical Logic, Hyperdoctrines, and Internal Languages
  1792. Lemma 143.27 — Equality is a congruenceCategorical Logic, Hyperdoctrines, and Internal Languages
  1793. Theorem 143.28 — The syntactic hyperdoctrineCategorical Logic, Hyperdoctrines, and Internal Languages
  1794. Theorem 143.30 — The canonical structure computes namesCategorical Logic, Hyperdoctrines, and Internal Languages
  1795. Proposition 144.3 — A tripos presents a hyperdoctrineTriposes, Toposes, and Realizability
  1796. Proposition 144.7 — The realizability preorderTriposes, Toposes, and Realizability
  1797. Lemma 144.14 — [ P] is a categoryTriposes, Toposes, and Realizability
  1798. Lemma 144.15 — Finite limitsTriposes, Toposes, and Realizability
  1799. Lemma 144.17 — MonomorphismsTriposes, Toposes, and Realizability
  1800. Lemma 144.19 — Subobjects are canonicalTriposes, Toposes, and Realizability
  1801. Theorem 144.20 — Power objectsTriposes, Toposes, and Realizability
  1802. Corollary 144.21 — [ P] is a toposTriposes, Toposes, and Realizability
  1803. Theorem 144.23 — Endomorphisms of NTriposes, Toposes, and Realizability
  1804. Theorem 144.25 — PittsTriposes, Toposes, and Realizability
  1805. Lemma 145.7 — Orthogonality is a Galois connectionClassical Realizability, Poles, and Orthogonality
  1806. Lemma 145.11 — Truth values of quantifiersClassical Realizability, Poles, and Orthogonality
  1807. Proposition 145.13 — Typing a continuation constantClassical Realizability, Poles, and Orthogonality
  1808. Theorem 145.14 — cc realizes Peirce's lawClassical Realizability, Poles, and Orthogonality
  1809. Proposition 145.16 — Behavior determines the formulaClassical Realizability, Poles, and Orthogonality
  1810. Lemma 145.20 — Substitution in falsity valuesClassical Realizability, Poles, and Orthogonality
  1811. Theorem 145.21 — AdequacyClassical Realizability, Poles, and Orthogonality
  1812. Corollary 145.22 — Proofs give universal realizersClassical Realizability, Poles, and Orthogonality
  1813. Corollary 145.23 — ConsistencyClassical Realizability, Poles, and Orthogonality
  1814. Lemma 116.10 — Extension commutes with substitutionAlgebraic Syntax, CwFs, and Initiality
  1815. Lemma 54.12 — Substitution eliminationAlgebraic Syntax, CwFs, and Initiality
  1816. Theorem 54.13 — Equivalence of the presentationsAlgebraic Syntax, CwFs, and Initiality
  1817. Lemma 54.18 — Terms are sectionsAlgebraic Syntax, CwFs, and Initiality
  1818. Lemma 54.20 — Comprehension is a pullbackAlgebraic Syntax, CwFs, and Initiality
  1819. Lemma 116.32 — Indexed interpretation and derivation independenceAlgebraic Syntax, CwFs, and Initiality
  1820. Theorem 54.27 — The term model and initialityAlgebraic Syntax, CwFs, and Initiality
  1821. Theorem 54.28 — Soundness of the interpretationAlgebraic Syntax, CwFs, and Initiality
  1822. Corollary 54.30 — Equivalence of structural presentationsAlgebraic Syntax, CwFs, and Initiality
  1823. Proposition 54.31 — The set model as a CwFAlgebraic Syntax, CwFs, and Initiality
  1824. Theorem 54.34 — The groupoid modelAlgebraic Syntax, CwFs, and Initiality
  1825. Proposition 54.35Algebraic Syntax, CwFs, and Initiality
  1826. Corollary 54.36 — K and UIP are underivableAlgebraic Syntax, CwFs, and Initiality
  1827. Lemma 147.5 — Extensions carry uniform families forwardGeneralized Algebraic Theories
  1828. Theorem 147.9 — InitialityGeneralized Algebraic Theories
  1829. Corollary 147.10 — Uniform families are contexts of the initial modelGeneralized Algebraic Theories
  1830. Theorem 147.11 — Structural inductionGeneralized Algebraic Theories
  1831. Proposition 147.13 — Interpretation into the first-order accountGeneralized Algebraic Theories
  1832. Proposition 148.4 — σ terminates and is confluentExplicit-Substitution Calculi
  1833. Proposition 148.5 — σ -normal forms are ordinary termsExplicit-Substitution Calculi
  1834. Theorem 148.6 — Simulation of βExplicit-Substitution Calculi
  1835. Theorem 148.7 — Confluence of λ σExplicit-Substitution Calculi
  1836. Theorem 148.8 — Composition breaks preservation of strong normalizationExplicit-Substitution Calculi
  1837. Theorem 148.13 — Full compositionExplicit-Substitution Calculi
  1838. Corollary 148.14 — SimulationExplicit-Substitution Calculi
  1839. Proposition 148.15 — The counterexample is blockedExplicit-Substitution Calculi
  1840. Theorem 148.16 — Imported properties of λ exExplicit-Substitution Calculi
  1841. Lemma 149.4Categorical Semantics of Scoped Operations
  1842. Proposition 149.6 — Scoped algebras are ordinary algebrasCategorical Semantics of Scoped Operations
  1843. Lemma 149.9 — Reading the free monad indexwiseCategorical Semantics of Scoped Operations
  1844. Theorem 149.10 — The projection adjunctionCategorical Semantics of Scoped Operations
  1845. Theorem 149.12 — The two monads agreeCategorical Semantics of Scoped Operations
  1846. Lemma 150.3 — Composition and functor actionCategorical Semantics of Coeffects
  1847. Theorem 150.9 — Soundness of the flat interpretationCategorical Semantics of Coeffects
  1848. Proposition 150.11 — The three models are instancesCategorical Semantics of Coeffects
  1849. Lemma 151.4 — The data are setsSet and CwF Models of Type Theory
  1850. Lemma 151.5 — Strict functorialitySet and CwF Models of Type Theory
  1851. Lemma 151.6 — ComprehensionSet and CwF Models of Type Theory
  1852. Lemma 151.7 — Comprehension squares are pullbacksSet and CwF Models of Type Theory
  1853. Proposition 151.8 — S is a CwFSet and CwF Models of Type Theory
  1854. Proposition 151.11 — Π - and Σ -structureSet and CwF Models of Type Theory
  1855. Proposition 151.12 — , , ,Set and CwF Models of Type Theory
  1856. Proposition 151.13 — W-typesSet and CwF Models of Type Theory
  1857. Proposition 151.14 — Identity typesSet and CwF Models of Type Theory
  1858. Proposition 151.16 — Universes and the exact use of inaccessibilitySet and CwF Models of Type Theory
  1859. Theorem 151.17 — Soundness of the set interpretationSet and CwF Models of Type Theory
  1860. Corollary 151.18 — ConsistencySet and CwF Models of Type Theory
  1861. Corollary 151.19 — The two booleans are not identifiedSet and CwF Models of Type Theory
  1862. Corollary 151.20 — Extensional type theory is consistent relative to the metatheorySet and CwF Models of Type Theory
  1863. Proposition 151.21 — The set model cannot separate from uniquenessSet and CwF Models of Type Theory
  1864. Corollary 151.23 — Interpretation of derivations is derivation-independentSet and CwF Models of Type Theory
  1865. Lemma 151.24 — Families are slicesSet and CwF Models of Type Theory
  1866. Proposition 151.25 — Σ and Π are the slice adjointsSet and CwF Models of Type Theory
  1867. Corollary 151.26Set and CwF Models of Type Theory
  1868. Proposition 151.27 — Chosen pullbacks are not strictly functorialSet and CwF Models of Type Theory
  1869. Lemma 151.31 — The glued total modelSet and CwF Models of Type Theory
  1870. Theorem 151.32 — Initiality supplies a sectionSet and CwF Models of Type Theory
  1871. Corollary 151.34 — Canonicity for the frozen fragmentSet and CwF Models of Type Theory
  1872. Lemma 152.5 — Gpd is cartesian closedGroupoid and Path-Object Models of Intensional Type Theory
  1873. Lemma 152.7 — Reindexing is strictly functorialGroupoid and Path-Object Models of Intensional Type Theory
  1874. Lemma 152.9 — The extension is a groupoid and _A is a dependent objectGroupoid and Path-Object Models of Intensional Type Theory
  1875. Proposition 152.10 — The groupoid CwFGroupoid and Path-Object Models of Intensional Type Theory
  1876. Lemma 152.12 — I_A is a family and r_A a dependent objectGroupoid and Path-Object Models of Intensional Type Theory
  1877. Lemma 152.13 — Every identity datum receives an arrow from a reflexivity datumGroupoid and Path-Object Models of Intensional Type Theory
  1878. Theorem 152.14 — Identity elimination in GGroupoid and Path-Object Models of Intensional Type Theory
  1879. Theorem 152.17 — Independence of uniqueness of identity proofsGroupoid and Path-Object Models of Intensional Type Theory
  1880. Proposition 152.18 — The eliminator has no interpretationGroupoid and Path-Object Models of Intensional Type Theory
  1881. Proposition 152.20 — Congruence of the second projection failsGroupoid and Path-Object Models of Intensional Type Theory
  1882. Proposition 152.22 — Identity on the universe is isomorphismGroupoid and Path-Object Models of Intensional Type Theory
  1883. Proposition 152.23 — Function extensionality holdsGroupoid and Path-Object Models of Intensional Type Theory
  1884. Proposition 152.26 — Gpd has path objectsGroupoid and Path-Object Models of Intensional Type Theory
  1885. Corollary 152.27 — The identity family is the path object of a typeGroupoid and Path-Object Models of Intensional Type Theory
  1886. Proposition 153.5 — ReplacementSetoid and PER Models of Type Theory
  1887. Lemma 153.7 — Transports are isomorphismsSetoid and PER Models of Type Theory
  1888. Lemma 153.9 — on Σ is an equivalence relationSetoid and PER Models of Type Theory
  1889. Proposition 153.10 — Reindexing is strictly functorialSetoid and PER Models of Type Theory
  1890. Theorem 153.11 — The setoid modelSetoid and PER Models of Type Theory
  1891. Proposition 153.12 — Π - and Σ -structureSetoid and PER Models of Type Theory
  1892. Proposition 153.13 — Natural numbers and sumsSetoid and PER Models of Type Theory
  1893. Proposition 153.14 — The equality type is the carried equalitySetoid and PER Models of Type Theory
  1894. Proposition 153.17 — Bracket structureSetoid and PER Models of Type Theory
  1895. Lemma 153.20 — =_V is an equivalence relation valued in _0Setoid and PER Models of Type Theory
  1896. Proposition 153.22 — κ is a family over VSetoid and PER Models of Type Theory
  1897. Theorem 153.23 — The universe of small setoidsSetoid and PER Models of Type Theory
  1898. Theorem 153.25 — Soundness for the listed rulesSetoid and PER Models of Type Theory
  1899. Lemma 153.29 — PER is a category with finite productsSetoid and PER Models of Type Theory
  1900. Proposition 153.31 — The PER modelSetoid and PER Models of Type Theory
  1901. Theorem 153.32 — The shared fragmentSetoid and PER Models of Type Theory
  1902. Lemma 154.3 — Unique analysisRecursive Domain Semantics and Computational Adequacy
  1903. Theorem 154.5 — Termination for the recursion-free fragmentRecursive Domain Semantics and Computational Adequacy
  1904. Proposition 154.6 — Two descriptions of |M| agreeRecursive Domain Semantics and Computational Adequacy
  1905. Lemma 154.9 — Embedding–projection pairsRecursive Domain Semantics and Computational Adequacy
  1906. Theorem 154.10 — The tree domain solves its equationRecursive Domain Semantics and Computational Adequacy
  1907. Lemma 154.12 — | | is well defined and satisfies its equationRecursive Domain Semantics and Computational Adequacy
  1908. Lemma 154.15 — Values are effect-freeRecursive Domain Semantics and Computational Adequacy
  1909. Lemma 154.16 — Equational soundnessRecursive Domain Semantics and Computational Adequacy
  1910. Theorem 154.17 — Adequacy, recursion-freeRecursive Domain Semantics and Computational Adequacy
  1911. Lemma 154.18 — Interpretation of infinitary effect valuesRecursive Domain Semantics and Computational Adequacy
  1912. Lemma 154.19 — The easy inequalityRecursive Domain Semantics and Computational Adequacy
  1913. Lemma 154.21 — Termination in ARecursive Domain Semantics and Computational Adequacy
  1914. Lemma 154.22 — Transfer alongRecursive Domain Semantics and Computational Adequacy
  1915. Proposition 154.23 — Approximants of the treeRecursive Domain Semantics and Computational Adequacy
  1916. Theorem 154.24 — Adequacy for recursionRecursive Domain Semantics and Computational Adequacy
  1917. Corollary 154.26 — Adequacy for nondeterminismRecursive Domain Semantics and Computational Adequacy
  1918. Corollary 154.27 — The ground-type statementRecursive Domain Semantics and Computational Adequacy
  1919. Lemma 155.3 — V is a partial combinatory algebraDependent PER-Enriched Domain Models
  1920. Proposition 155.5 — Monotonicity repairs the Σ -argumentDependent PER-Enriched Domain Models
  1921. Lemma 155.9 — Split reindexingDependent PER-Enriched Domain Models
  1922. Theorem 155.10 — ComprehensionDependent PER-Enriched Domain Models
  1923. Proposition 155.11 — Dependent products and sumsDependent PER-Enriched Domain Models
  1924. Theorem 155.12 — Monotone completion is a reflectionDependent PER-Enriched Domain Models
  1925. Corollary 155.13 — Impredicative sumsDependent PER-Enriched Domain Models
  1926. Lemma 155.15 — u is continuousDependent PER-Enriched Domain Models
  1927. Theorem 155.16 — Fixed points at admissible typesDependent PER-Enriched Domain Models
  1928. Theorem 155.18 — Semantic substitution and soundnessDependent PER-Enriched Domain Models
  1929. Lemma 156.5 — Strict stability is what the syntax needsCoherence and Local Universes
  1930. Lemma 156.7 — C_! is a split full comprehension categoryCoherence and Local Universes
  1931. Proposition 156.10 — Sufficient conditionsCoherence and Local Universes
  1932. Lemma 156.13 — Sums are strictly stable in C_!Coherence and Local Universes
  1933. Lemma 156.15 — The representing propertyCoherence and Local Universes
  1934. Theorem 156.17 — Π is strictly stable in C_!Coherence and Local Universes
  1935. Theorem 156.18 — CoherenceCoherence and Local Universes
  1936. Corollary 156.19 — The slice interpretation is repairedCoherence and Local Universes
  1937. Lemma 157.5 — Views are justified sequencesGames, Arenas, and Strategies
  1938. Lemma 157.8 — SwitchingGames, Arenas, and Strategies
  1939. Proposition 157.9 — Composition is a strategyGames, Arenas, and Strategies
  1940. Theorem 157.11 — The category of gamesGames, Arenas, and Strategies
  1941. Proposition 157.13 — Innocence and bracketing are preservedGames, Arenas, and Strategies
  1942. Corollary 157.14 — Innocent subcategoryGames, Arenas, and Strategies
  1943. Proposition 157.15 — ProductsGames, Arenas, and Strategies
  1944. Proposition 157.16 — ExponentialsGames, Arenas, and Strategies
  1945. Lemma 157.18 — Strategies form a pointed dcpoGames, Arenas, and Strategies
  1946. Proposition 157.20 — SoundnessGames, Arenas, and Strategies
  1947. Theorem 157.21 — Computational adequacyGames, Arenas, and Strategies
  1948. Lemma 158.2 — Context lemmaDefinability and Full Abstraction for PCF
  1949. Proposition 158.3 — Soundness gives one halfDefinability and Full Abstraction for PCF
  1950. Lemma 158.5 — The quotient is a cartesian closed categoryDefinability and Full Abstraction for PCF
  1951. Lemma 158.7 — Compact approximationDefinability and Full Abstraction for PCF
  1952. Lemma 158.9 — First moveDefinability and Full Abstraction for PCF
  1953. Lemma 158.10 — DecompositionDefinability and Full Abstraction for PCF
  1954. Theorem 158.11 — DefinabilityDefinability and Full Abstraction for PCF
  1955. Theorem 158.13 — Inequational full abstractionDefinability and Full Abstraction for PCF
  1956. Corollary 158.14 — Equational full abstractionDefinability and Full Abstraction for PCF
  1957. Corollary 158.15 — Why the quotient is neededDefinability and Full Abstraction for PCF
  1958. Proposition 159.3 — The pentagon is forcedSymmetric Monoidal Categories and Graphical Linear Semantics
  1959. Proposition 159.4 — The triangle is forcedSymmetric Monoidal Categories and Graphical Linear Semantics
  1960. Lemma 159.6 — Two derived unit equationsSymmetric Monoidal Categories and Graphical Linear Semantics
  1961. Proposition 159.8 — Braided but not symmetricSymmetric Monoidal Categories and Graphical Linear Semantics
  1962. Theorem 159.12 — Normal form and decidable equalitySymmetric Monoidal Categories and Graphical Linear Semantics
  1963. Theorem 159.15 — Soundness and completeness for the free fragmentSymmetric Monoidal Categories and Graphical Linear Semantics
  1964. Lemma 159.18 — The two inverse lawsSymmetric Monoidal Categories and Graphical Linear Semantics
  1965. Lemma 159.20 — Independence of the split isomorphismSymmetric Monoidal Categories and Graphical Linear Semantics
  1966. Theorem 159.21 — Semantic substitution and soundnessSymmetric Monoidal Categories and Graphical Linear Semantics
  1967. Proposition 159.23 — Declaring objects copyable is not enoughSymmetric Monoidal Categories and Graphical Linear Semantics
  1968. Theorem 159.25 — The exponential comonadSymmetric Monoidal Categories and Graphical Linear Semantics
  1969. Corollary 159.26 — Interpretation of the full calculusSymmetric Monoidal Categories and Graphical Linear Semantics
  1970. Proposition 159.29 — Preservation equations for the interpretationSymmetric Monoidal Categories and Graphical Linear Semantics
  1971. Lemma 160.2 — Weakening and substitutionModal and Multimodal Dependent Type Theory
  1972. Proposition 160.3 — Normalization by evaluation, one calculationModal and Multimodal Dependent Type Theory
  1973. Theorem 160.7 — Soundness at the exact signatureModal and Multimodal Dependent Type Theory
  1974. Lemma 160.12 — Weakening and substitution, multimodallyModal and Multimodal Dependent Type Theory
  1975. Theorem 160.13 — Canonicity for the frozen mode theoryModal and Multimodal Dependent Type Theory
  1976. Proposition 160.16 — Guarded recursion is typableModal and Multimodal Dependent Type Theory
  1977. Lemma 161.11 — The modalities are idempotent monadsSynthetic Phase Distinctions and Synthetic Tait Computability
  1978. Lemma 161.13 — Closed-modality criterionSynthetic Phase Distinctions and Synthetic Tait Computability
  1979. Lemma 161.15 — Computation of the modalities in GSynthetic Phase Distinctions and Synthetic Tait Computability
  1980. Theorem 161.16 — FractureSynthetic Phase Distinctions and Synthetic Tait Computability
  1981. Lemma 161.18 — Extents are closed-modalSynthetic Phase Distinctions and Synthetic Tait Computability
  1982. Lemma 161.22 — Open and closed subuniversesSynthetic Phase Distinctions and Synthetic Tait Computability
  1983. Proposition 161.24 — Glue types from realignmentSynthetic Phase Distinctions and Synthetic Tait Computability
  1984. Lemma 161.25 — Interpretation of the glue type in GSynthetic Phase Distinctions and Synthetic Tait Computability
  1985. Proposition 161.30 — The eliminator is well definedSynthetic Phase Distinctions and Synthetic Tait Computability
  1986. Proposition 161.32 — The product clauses are well typedSynthetic Phase Distinctions and Synthetic Tait Computability
  1987. Theorem 161.33 — Fundamental theorem for the gluing model; importedSynthetic Phase Distinctions and Synthetic Tait Computability
  1988. Theorem 161.34 — CanonicitySynthetic Phase Distinctions and Synthetic Tait Computability
  1989. Proposition 162.4 — Dependent applicationGuarded and Clocked Dependent Type Theory
  1990. Proposition 162.6 — Uniqueness of guarded fixed pointsGuarded and Clocked Dependent Type Theory
  1991. Lemma 162.11 — Preservation of finite limitsGuarded and Clocked Dependent Type Theory
  1992. Theorem 162.14 — Unique guarded fixed pointsGuarded and Clocked Dependent Type Theory
  1993. Theorem 162.16 — SoundnessGuarded and Clocked Dependent Type Theory
  1994. Theorem 162.18 — The guarded stream objectGuarded and Clocked Dependent Type Theory
  1995. Proposition 162.20 — The observation is well definedGuarded and Clocked Dependent Type Theory
  1996. Theorem 162.21 — Productivity of finite observationsGuarded and Clocked Dependent Type Theory
  1997. Lemma 162.25 — Clock quantification is trivial on clock-free typesGuarded and Clocked Dependent Type Theory
  1998. Theorem 162.28 — Bisimulation for guarded streamsGuarded and Clocked Dependent Type Theory
  1999. Lemma 163.2 — ExponentialsSynthetic Guarded Domain Theory and Step-Indexed Semantics
  2000. Proposition 163.4 — The later operator is a predicate formerSynthetic Guarded Domain Theory and Step-Indexed Semantics
  2001. Theorem 163.5 — L"ob inductionSynthetic Guarded Domain Theory and Step-Indexed Semantics
  2002. Proposition 163.7 — L solves its equation, uniquelySynthetic Guarded Domain Theory and Step-Indexed Semantics
  2003. Proposition 163.9 — Monad lawsSynthetic Guarded Domain Theory and Step-Indexed Semantics
  2004. Theorem 163.11 — Solution of the equationSynthetic Guarded Domain Theory and Step-Indexed Semantics
  2005. Proposition 163.15 — Every divergence reads the cellSynthetic Guarded Domain Theory and Step-Indexed Semantics
  2006. Lemma 163.17 — Evaluation contextsSynthetic Guarded Domain Theory and Step-Indexed Semantics
  2007. Lemma 163.18 — SubstitutionSynthetic Guarded Domain Theory and Step-Indexed Semantics
  2008. Theorem 163.19 — Soundness of the interpretationSynthetic Guarded Domain Theory and Step-Indexed Semantics
  2009. Corollary 163.20 — Reading is the only step the model countsSynthetic Guarded Domain Theory and Step-Indexed Semantics
  2010. Lemma 163.22 — Determinism and progressSynthetic Guarded Domain Theory and Step-Indexed Semantics
  2011. Theorem 163.23 — Adequacy atSynthetic Guarded Domain Theory and Step-Indexed Semantics
  2012. Lemma 163.25 — The relations are predicatesSynthetic Guarded Domain Theory and Step-Indexed Semantics
  2013. Theorem 163.26 — Fundamental lemmaSynthetic Guarded Domain Theory and Step-Indexed Semantics
  2014. Corollary 163.27 — Adequacy at every typeSynthetic Guarded Domain Theory and Step-Indexed Semantics
  2015. Theorem 163.28 — Denotational equality implies contextual equivalenceSynthetic Guarded Domain Theory and Step-Indexed Semantics
  2016. Theorem 163.30 — Least fixed pointsSynthetic Guarded Domain Theory and Step-Indexed Semantics
  2017. Proposition 163.31 — Fixed-point inductionSynthetic Guarded Domain Theory and Step-Indexed Semantics
  2018. Proposition 164.2 — Abstraction for simple typesDependent Parametricity
  2019. Proposition 164.3 — The identity free theoremDependent Parametricity
  2020. Lemma 164.8 — Translation commutes with substitutionDependent Parametricity
  2021. Theorem 164.9 — AbstractionDependent Parametricity
  2022. Corollary 164.10 — Closed terms are self-relatedDependent Parametricity
  2023. Lemma 164.13 — Identity extension atDependent Parametricity
  2024. Theorem 164.14 — Representation independence for the counterDependent Parametricity
  2025. Proposition 164.17 — Identity extension is at least function extensionalityDependent Parametricity
  2026. Proposition 164.20 — The axiom has no local interpretationDependent Parametricity
  2027. Proposition 164.21 — The axiom breaks canonicityDependent Parametricity
  2028. Lemma 165.8 — The two size variances are forcedSized Copattern Recursion and Mixed Induction–Coinduction
  2029. Lemma 165.10 — The fixed points at ∞Sized Copattern Recursion and Mixed Induction–Coinduction
  2030. Proposition 165.18 — The block type-checksSized Copattern Recursion and Mixed Induction–Coinduction
  2031. Lemma 165.22 — Multi-clause objects and symbolsSized Copattern Recursion and Mixed Induction–Coinduction
  2032. Lemma 165.24 — The function space is a candidateSized Copattern Recursion and Mixed Induction–Coinduction
  2033. Lemma 165.26 — Pre- and post-fixed pointsSized Copattern Recursion and Mixed Induction–Coinduction
  2034. Lemma 165.27 — Fixed pointsSized Copattern Recursion and Mixed Induction–Coinduction
  2035. Theorem 165.29 — Soundness of expression typingSized Copattern Recursion and Mixed Induction–Coinduction
  2036. Theorem 165.30 — Soundness of block typingSized Copattern Recursion and Mixed Induction–Coinduction
  2037. Corollary 165.31 — Strong normalizationSized Copattern Recursion and Mixed Induction–Coinduction
  2038. Corollary 165.32 — Termination and productivity of the stream processorSized Copattern Recursion and Mixed Induction–Coinduction
  2039. Proposition 166.1 — A largest size destroys well-founded inductionParametric Large Sizes and Realizability Consistency
  2040. Lemma 166.6 — Uniqueness of fixed pointsParametric Large Sizes and Realizability Consistency
  2041. Proposition 166.7 — Two equivalences that are already derivableParametric Large Sizes and Realizability Consistency
  2042. Proposition 166.9 — Quantification over a size-free type is trivialParametric Large Sizes and Realizability Consistency
  2043. Lemma 166.12 — Size-indexed initial algebraParametric Large Sizes and Realizability Consistency
  2044. Lemma 166.13 — Constant size-indexed algebrasParametric Large Sizes and Realizability Consistency
  2045. Proposition 166.15 — Quantifying an algebraParametric Large Sizes and Realizability Consistency
  2046. Theorem 166.16 — Initial algebras from large sizesParametric Large Sizes and Realizability Consistency
  2047. Proposition 166.17 — Polynomial functors weakly commuteParametric Large Sizes and Realizability Consistency
  2048. Corollary 166.18 — W-typesParametric Large Sizes and Realizability Consistency
  2049. Theorem 166.20 — Final coalgebras from large sizesParametric Large Sizes and Realizability Consistency
  2050. Lemma 166.25 — Modest sets are partial equivalence relationsParametric Large Sizes and Realizability Consistency
  2051. Lemma 166.27 — Modest reflectionParametric Large Sizes and Realizability Consistency
  2052. Theorem 166.28 — Validation of the added rulesParametric Large Sizes and Realizability Consistency
  2053. Theorem 166.29 — ConsistencyParametric Large Sizes and Realizability Consistency
  2054. Proposition 167.6 — Spans of the four base formersInternal Parametricity without an Interval
  2055. Lemma 167.7 — Four derived equationsInternal Parametricity without an Interval
  2056. Theorem 167.9 — The two syntaxes agree; importedInternal Parametricity without an Interval
  2057. Lemma 167.11 — Generalized symmetriesInternal Parametricity without an Interval
  2058. Theorem 167.12 — Presheaf modelInternal Parametricity without an Interval
  2059. Lemma 167.14 — G preserves the span structureInternal Parametricity without an Interval
  2060. Theorem 167.15 — Boolean canonicityInternal Parametricity without an Interval
  2061. Theorem 167.16 — Uniqueness of the polymorphic identityInternal Parametricity without an Interval
  2062. Lemma 168.5 — Preservation and determinismReversible Classical Computation
  2063. Proposition 168.7 — Progress for exhaustive isosReversible Classical Computation
  2064. Proposition 168.9 — Inversion is an involutionReversible Classical Computation
  2065. Lemma 168.10 — Inversion is well typedReversible Classical Computation
  2066. Lemma 168.11 — Inversion commutes with evaluationReversible Classical Computation
  2067. Theorem 168.13 — The two directions agreeReversible Classical Computation
  2068. Proposition 168.15 — The example is well typed and self-inverse in one factorReversible Classical Computation
  2069. Proposition 168.18 — UncomputationReversible Classical Computation
  2070. Lemma 168.20 — PInj is symmetric monoidalReversible Classical Computation
  2071. Lemma 168.23 — The particle trace is a partial injectionReversible Classical Computation
  2072. Theorem 168.24 — The particle trace satisfies the trace lawsReversible Classical Computation
  2073. Lemma 168.27 — Clause sets denote partial injectionsReversible Classical Computation
  2074. Theorem 168.28 — Inversion denotes inversionReversible Classical Computation
  2075. Theorem 168.29 — SoundnessReversible Classical Computation
  2076. Theorem 168.30 — Adequacy; importedReversible Classical Computation
  2077. Proposition 169.2 — Composition of lensesProfunctors, Coends, and Optics
  2078. Proposition 169.8 — Where the structure comes fromProfunctors, Coends, and Optics
  2079. Proposition 169.11 — Ends and coends inProfunctors, Coends, and Optics
  2080. Lemma 169.12 — Yoneda reductionProfunctors, Coends, and Optics
  2081. Proposition 169.14 — Two actions onProfunctors, Coends, and Optics
  2082. Proposition 169.17 — CompositionProfunctors, Coends, and Optics
  2083. Proposition 169.18 — Lenses are optics for the product actionProfunctors, Coends, and Optics
  2084. Proposition 169.19 — Prisms are optics for the coproduct actionProfunctors, Coends, and Optics
  2085. Lemma 169.23 — Φ is left adjoint to UProfunctors, Coends, and Optics
  2086. Theorem 169.24 — Profunctor representationProfunctors, Coends, and Optics
  2087. Corollary 169.25 — Both directions, explicitlyProfunctors, Coends, and Optics
  2088. Theorem 169.28 — Lawfulness specialises to the lens lawsProfunctors, Coends, and Optics
  2089. Proposition 169.30 — Lawful optics composeProfunctors, Coends, and Optics
  2090. Proposition 169.31 — Lawfulness specialises to the prism lawsProfunctors, Coends, and Optics
  2091. Proposition 169.33 — Traversals are optics for that actionProfunctors, Coends, and Optics
  2092. Proposition 170.2 — Dependent lenses as maps over a baseDependent Optics and Indexed Bidirectional Structure
  2093. Theorem 170.6 — Optic_ L, R is a categoryDependent Optics and Indexed Bidirectional Structure
  2094. Proposition 170.7 — Mixed optics are the one-object caseDependent Optics and Indexed Bidirectional Structure
  2095. Proposition 170.8 — Functor lenses are the trivial-forward caseDependent Optics and Indexed Bidirectional Structure
  2096. Theorem 170.11 — The hom-set of dependent lensesDependent Optics and Indexed Bidirectional Structure
  2097. Lemma 170.13 — Coproducts in the span bicategoryDependent Optics and Indexed Bidirectional Structure
  2098. Proposition 170.14 — Coproducts of dependent opticsDependent Optics and Indexed Bidirectional Structure
  2099. Theorem 170.17 — Classification of contravariant functorsDependent Optics and Indexed Bidirectional Structure
  2100. Corollary 170.18 — Profunctor encoding of dependent opticsDependent Optics and Indexed Bidirectional Structure
  2101. Lemma 171.7 — Monotone approximationProbabilistic Lambda Calculi and Program Equivalence
  2102. Lemma 171.9 — Path decompositionProbabilistic Lambda Calculi and Program Equivalence
  2103. Lemma 171.15 — What a test measuresProbabilistic Lambda Calculi and Program Equivalence
  2104. Lemma 171.18 — ClosureProbabilistic Lambda Calculi and Program Equivalence
  2105. Lemma 171.20 — Downward closure and increasing limitsProbabilistic Lambda Calculi and Program Equivalence
  2106. Proposition 171.24 — The arrow is a probabilistic coherence spaceProbabilistic Lambda Calculi and Program Equivalence
  2107. Lemma 171.25 — The invariants of the interpreted typesProbabilistic Lambda Calculi and Program Equivalence
  2108. Lemma 171.26 — Coefficients from valuesProbabilistic Lambda Calculi and Program Equivalence
  2109. Theorem 171.27 — DeterminationProbabilistic Lambda Calculi and Program Equivalence
  2110. Lemma 171.31 — SubstitutionProbabilistic Lambda Calculi and Program Equivalence
  2111. Theorem 171.32 — Invariance under one stepProbabilistic Lambda Calculi and Program Equivalence
  2112. Theorem 171.33 — The model dominates the operational semanticsProbabilistic Lambda Calculi and Program Equivalence
  2113. Lemma 171.35 — Zero and limitsProbabilistic Lambda Calculi and Program Equivalence
  2114. Lemma 171.36 — Convergence through a conditionalProbabilistic Lambda Calculi and Program Equivalence
  2115. Lemma 171.37 — One step backwardsProbabilistic Lambda Calculi and Program Equivalence
  2116. Theorem 171.38 — Fundamental lemmaProbabilistic Lambda Calculi and Program Equivalence
  2117. Theorem 171.39 — AdequacyProbabilistic Lambda Calculi and Program Equivalence
  2118. Lemma 171.40 — Contexts act on denotationsProbabilistic Lambda Calculi and Program Equivalence
  2119. Theorem 171.41 — Denotational equality implies observational equivalenceProbabilistic Lambda Calculi and Program Equivalence
  2120. Lemma 171.44 — Parameter budgetProbabilistic Lambda Calculi and Program Equivalence
  2121. Theorem 171.47 — SeparationProbabilistic Lambda Calculi and Program Equivalence
  2122. Theorem 171.48 — Observational equivalence implies denotational equalityProbabilistic Lambda Calculi and Program Equivalence
  2123. Corollary 171.49 — Equational full abstractionProbabilistic Lambda Calculi and Program Equivalence
  2124. Proposition 171.50 — The matrix order is finer than the pointwise orderProbabilistic Lambda Calculi and Program Equivalence
  2125. Proposition 172.5 — The two executions agree on the fragmentProbability, Measure, Kernels, and Computable Sampling
  2126. Lemma 172.7 — Identity and compositionProbability, Measure, Kernels, and Computable Sampling
  2127. Lemma 172.8 — Measurability from a generating familyProbability, Measure, Kernels, and Computable Sampling
  2128. Lemma 172.11 — Pushforward is functorialProbability, Measure, Kernels, and Computable Sampling
  2129. Lemma 172.13 — Monotonicity and indicatorsProbability, Measure, Kernels, and Computable Sampling
  2130. Theorem 172.14 — Change of variablesProbability, Measure, Kernels, and Computable Sampling
  2131. Lemma 172.15 — Dirac and productsProbability, Measure, Kernels, and Computable Sampling
  2132. Lemma 172.17 — The return kernel is a kernelProbability, Measure, Kernels, and Computable Sampling
  2133. Proposition 172.18 — Bind is well definedProbability, Measure, Kernels, and Computable Sampling
  2134. Lemma 172.19 — Integration against a bindProbability, Measure, Kernels, and Computable Sampling
  2135. Theorem 172.20 — Monad laws for kernelsProbability, Measure, Kernels, and Computable Sampling
  2136. Lemma 172.22 — Pushforward as a bind, and the mass boundProbability, Measure, Kernels, and Computable Sampling
  2137. Proposition 172.24 — Increasing chainsProbability, Measure, Kernels, and Computable Sampling
  2138. Proposition 172.25 — Bind preserves increasing supremaProbability, Measure, Kernels, and Computable Sampling
  2139. Lemma 172.29 — Uniqueness on a generating algebraProbability, Measure, Kernels, and Computable Sampling
  2140. Lemma 172.30 — Splitting produces an independent pairProbability, Measure, Kernels, and Computable Sampling
  2141. Theorem 172.32 — Pushforward correspondenceProbability, Measure, Kernels, and Computable Sampling
  2142. Proposition 173.4 — Versions agree almost everywhereComputable Conditioning and Its Limits
  2143. Lemma 173.9 — An arbitrary answer nearbyComputable Conditioning and Its Limits
  2144. Theorem 173.10 — Every conditioning operator is discontinuous everywhereComputable Conditioning and Its Limits
  2145. Proposition 173.13 — Discrete observationsComputable Conditioning and Its Limits
  2146. Proposition 173.15 — Bayes' rule under a positive bounded densityComputable Conditioning and Its Limits
  2147. Proposition 173.16 — Computability of Bayes' ruleComputable Conditioning and Its Limits
  2148. Corollary 173.17 — Observations corrupted by independent noiseComputable Conditioning and Its Limits
  2149. Lemma 174.2 — Countable dependenceContinuous Probabilistic Languages and Quasi-Borel Semantics
  2150. Theorem 174.3 — The evaluation σ -algebra failsContinuous Probabilistic Languages and Quasi-Borel Semantics
  2151. Proposition 174.8 — ProductsContinuous Probabilistic Languages and Quasi-Borel Semantics
  2152. Proposition 174.9 — Countable coproductsContinuous Probabilistic Languages and Quasi-Borel Semantics
  2153. Proposition 174.10 — Function spacesContinuous Probabilistic Languages and Quasi-Borel Semantics
  2154. Lemma 174.13 — P(X) is a quasi-Borel spaceContinuous Probabilistic Languages and Quasi-Borel Semantics
  2155. Lemma 174.15 — Bind is well definedContinuous Probabilistic Languages and Quasi-Borel Semantics
  2156. Theorem 174.16 — The probability monadContinuous Probabilistic Languages and Quasi-Borel Semantics
  2157. Proposition 174.17 — CommutativityContinuous Probabilistic Languages and Quasi-Borel Semantics
  2158. Lemma 175.8 — Transformations composeInference as Semantics-Preserving Program Transformation
  2159. Proposition 175.11 — Importance weighting on one stepInference as Semantics-Preserving Program Transformation
  2160. Lemma 175.15 — Suspension steps preserve meaningInference as Semantics-Preserving Program Transformation
  2161. Lemma 175.16 — Spawning preserves meaningInference as Semantics-Preserving Program Transformation
  2162. Lemma 175.17 — The discrete weighted randomiserInference as Semantics-Preserving Program Transformation
  2163. Proposition 175.18 — Resampling preserves meaningInference as Semantics-Preserving Program Transformation
  2164. Theorem 175.20 — The sequential Monte Carlo compositeInference as Semantics-Preserving Program Transformation
  2165. Proposition 176.5 — InterderivabilityProbabilistic Program Logics
  2166. Theorem 176.7 — Soundness for the fragmentProbabilistic Program Logics
  2167. Proposition 176.10 — Removing an unused drawProbabilistic Program Logics
  2168. Lemma 176.12 — Markov and ChebyshevProbabilistic Program Logics
  2169. Proposition 176.13 — Monte Carlo sample sizeProbabilistic Program Logics
  2170. Lemma 177.3 — Two steps composeExpected Cost and Probabilistic Resource Analysis
  2171. Theorem 177.10 — Soundness for terminating massExpected Cost and Probabilistic Resource Analysis
  2172. Theorem 177.14 — Improved soundnessExpected Cost and Probabilistic Resource Analysis
  2173. Corollary 177.15 — Almost sure termination, under the tick hypothesisExpected Cost and Probabilistic Resource Analysis
  2174. Lemma 178.4 — Avoiding a list of outcomesError Credits and Approximate Higher-Order Reasoning
  2175. Theorem 178.7 — Adequacy for the finite fragmentError Credits and Approximate Higher-Order Reasoning
  2176. Lemma 178.10 — The interface laws hold in the modelError Credits and Approximate Higher-Order Reasoning
  2177. Lemma 179.3 — f N is a measure, and densities compose with mixturesVerified Compilation of Probabilistic Programs
  2178. Lemma 179.4 — Densities are unique almost everywhereVerified Compilation of Probabilistic Programs
  2179. Lemma 179.9 — Two representative soundness casesVerified Compilation of Probabilistic Programs
  2180. Proposition 180.3 — Strict functorialityDependent Probability and Fibred Measure
  2181. Proposition 180.9 — The family fibration is split, and comprehension is a morphismDependent Probability and Fibred Measure
  2182. Proposition 180.12 — Reindexing commutes with the fibred monadsDependent Probability and Fibred Measure
  2183. Theorem 181.5 — Confluence of the differential calculus; importedDifferential Lambda Calculus and Resource Taylor Expansion
  2184. Lemma 181.8 — Differential substitution is placementDifferential Lambda Calculus and Resource Taylor Expansion
  2185. Lemma 181.12 — Size strictly decreasesDifferential Lambda Calculus and Resource Taylor Expansion
  2186. Lemma 181.13 — Symmetry of the second derivativeDifferential Lambda Calculus and Resource Taylor Expansion
  2187. Lemma 181.14 — Reduction commutes with placementDifferential Lambda Calculus and Resource Taylor Expansion
  2188. Theorem 181.15 — Church–Rosser and strong normalizationDifferential Lambda Calculus and Resource Taylor Expansion
  2189. Lemma 181.22 — Members of an expansion are uniform and pairwise coherentDifferential Lambda Calculus and Resource Taylor Expansion
  2190. Theorem 181.23 — Uniformity and multiplicity; importedDifferential Lambda Calculus and Resource Taylor Expansion
  2191. Theorem 181.26 — Normal resource terms come from B"ohm trees; importedDifferential Lambda Calculus and Resource Taylor Expansion
  2192. Theorem 181.27 — Normalization commutes with expansion; importedDifferential Lambda Calculus and Resource Taylor Expansion
  2193. Lemma 182.7 — The macro preserves typingDifferentiable Semantics and Forward-Mode Automatic Differentiation
  2194. Lemma 182.11 — Fundamental lemmaDifferentiable Semantics and Forward-Mode Automatic Differentiation
  2195. Theorem 182.12 — Correctness at a first-order interfaceDifferentiable Semantics and Forward-Mode Automatic Differentiation
  2196. Theorem 182.14 — Higher order and all first-order types; importedDifferentiable Semantics and Forward-Mode Automatic Differentiation
  2197. Theorem 183.5 — Correctness of the reverse macroReverse-Mode Automatic Differentiation and Cotangent Semantics
  2198. Theorem 183.7 — Correctness at first-order interfaces; importedReverse-Mode Automatic Differentiation and Cotangent Semantics
  2199. Theorem 183.9 — Asymptotic efficiency; importedReverse-Mode Automatic Differentiation and Cotangent Semantics
  2200. Lemma 184.3 — The Bell state is entangledQuantum Lambda Calculi and Linear Quantum Data
  2201. Theorem 184.4 — No cloningQuantum Lambda Calculi and Linear Quantum Data
  2202. Lemma 184.14 — Weakening and duplicable valuesQuantum Lambda Calculi and Linear Quantum Data
  2203. Lemma 184.15 — Linear substitutionQuantum Lambda Calculi and Linear Quantum Data
  2204. Theorem 184.16 — Subject reductionQuantum Lambda Calculi and Linear Quantum Data
  2205. Lemma 184.17 — Shape of valuesQuantum Lambda Calculi and Linear Quantum Data
  2206. Theorem 184.18 — Progress and safetyQuantum Lambda Calculi and Linear Quantum Data
  2207. Corollary 184.19 — What the type system establishesQuantum Lambda Calculi and Linear Quantum Data
  2208. Proposition 184.21 — No principal typesQuantum Lambda Calculi and Linear Quantum Data
  2209. Theorem 184.23 — Decoration is sound and complete for typabilityQuantum Lambda Calculi and Linear Quantum Data
  2210. Proposition 184.28 — Hilbert spaces are compact closedQuantum Lambda Calculi and Linear Quantum Data
  2211. Proposition 184.30 — Typing soundness for the unitary fragmentQuantum Lambda Calculi and Linear Quantum Data
  2212. Theorem 185.9 — Safety and soundness for Proto-Quipper-M; importedTyped Quantum Circuits and Proto-Quipper-M
  2213. Lemma 185.10 — The boxing case of soundnessTyped Quantum Circuits and Proto-Quipper-M
  2214. Theorem 186.4 — Shape preserves typingLinear-Dependent Quantum Programming and Proto-Quipper-D
  2215. Theorem 186.5 — SubstitutionLinear-Dependent Quantum Programming and Proto-Quipper-D
  2216. Theorem 186.6 — Type preservationLinear-Dependent Quantum Programming and Proto-Quipper-D
  2217. Lemma 187.4 — The metric caseElementary Topology and Classical Homotopy
  2218. Lemma 187.5 — Composites and restrictionsElementary Topology and Classical Homotopy
  2219. Lemma 187.7 — Maps into a productElementary Topology and Classical Homotopy
  2220. Lemma 187.10 — Intervals are connectedElementary Topology and Classical Homotopy
  2221. Lemma 187.11 — Gluing along closed piecesElementary Topology and Classical Homotopy
  2222. Lemma 187.13 — Heine–Borel for the unit intervalElementary Topology and Classical Homotopy
  2223. Lemma 187.14 — Compactness transfersElementary Topology and Classical Homotopy
  2224. Proposition 187.15 — Continuous bijections out of compact spacesElementary Topology and Classical Homotopy
  2225. Proposition 187.19 — Path homotopy is an equivalence relationElementary Topology and Classical Homotopy
  2226. Lemma 187.20 — ReparametrizationElementary Topology and Classical Homotopy
  2227. Theorem 187.21 — Concatenation adds windingElementary Topology and Classical Homotopy
  2228. Proposition 187.25 — Retraction gives equivalenceElementary Topology and Classical Homotopy
  2229. Theorem 187.26 — The punctured plane deforms onto the circleElementary Topology and Classical Homotopy
  2230. Lemma 187.33 — Universal property of a quotientElementary Topology and Classical Homotopy
  2231. Lemma 187.35 — Mapping out of a pushoutElementary Topology and Classical Homotopy
  2232. Theorem 187.38 — Suspending the circleElementary Topology and Classical Homotopy
  2233. Lemma 188.2 — Fibers of a covering are discreteFibrations, Homotopy Groups, and Exact Sequences
  2234. Lemma 188.4 — Unique liftingFibrations, Homotopy Groups, and Exact Sequences
  2235. Lemma 188.5 — Lebesgue numberFibrations, Homotopy Groups, and Exact Sequences
  2236. Theorem 188.6 — Path liftingFibrations, Homotopy Groups, and Exact Sequences
  2237. Theorem 188.7 — Homotopy lifting for coveringsFibrations, Homotopy Groups, and Exact Sequences
  2238. Proposition 188.9 — π _1 is a groupFibrations, Homotopy Groups, and Exact Sequences
  2239. Proposition 188.11 — Functoriality and base-point changeFibrations, Homotopy Groups, and Exact Sequences
  2240. Theorem 188.12 — The fundamental group of the circleFibrations, Homotopy Groups, and Exact Sequences
  2241. Corollary 188.13 — The punctured planeFibrations, Homotopy Groups, and Exact Sequences
  2242. Corollary 188.14 — The circle is not contractibleFibrations, Homotopy Groups, and Exact Sequences
  2243. Proposition 188.16 — Two families of fibrationsFibrations, Homotopy Groups, and Exact Sequences
  2244. Proposition 188.17 — Pullbacks of fibrationsFibrations, Homotopy Groups, and Exact Sequences
  2245. Proposition 188.19 — π _n is a groupFibrations, Homotopy Groups, and Exact Sequences
  2246. Theorem 188.20 — Interchange and commutativityFibrations, Homotopy Groups, and Exact Sequences
  2247. Lemma 188.22 — Projection to the top faceFibrations, Homotopy Groups, and Exact Sequences
  2248. Lemma 188.23 — Coning a boundary homeomorphismFibrations, Homotopy Groups, and Exact Sequences
  2249. Proposition 188.24 — The cube pairFibrations, Homotopy Groups, and Exact Sequences
  2250. Corollary 188.25 — Lifting with one free faceFibrations, Homotopy Groups, and Exact Sequences
  2251. Lemma 188.27 — The connecting map is well definedFibrations, Homotopy Groups, and Exact Sequences
  2252. Lemma 188.28 — The connecting map is a homomorphismFibrations, Homotopy Groups, and Exact Sequences
  2253. Theorem 188.29 — Exact sequence of a fibrationFibrations, Homotopy Groups, and Exact Sequences
  2254. Theorem 188.30 — Homotopy groups of the circleFibrations, Homotopy Groups, and Exact Sequences
  2255. Corollary 188.32 — The torusFibrations, Homotopy Groups, and Exact Sequences
  2256. Proposition 62.2 — The groupoid structure, transcribedTypes as ∞-Groupoids
  2257. Lemma 62.4 — The horizontal composites agreeTypes as ∞-Groupoids
  2258. Lemma 62.6 — Identity and constant functionsTypes as ∞-Groupoids
  2259. Lemma 62.7 — Transport is functorial in every argumentTypes as ∞-Groupoids
  2260. Lemma 62.8 — Transport in path familiesTypes as ∞-Groupoids
  2261. Lemma 62.12Types as ∞-Groupoids
  2262. Theorem 62.13 — Homotopies are naturalTypes as ∞-Groupoids
  2263. Corollary 62.14Types as ∞-Groupoids
  2264. Lemma 62.16 — Whiskering by reflexivity, one level upTypes as ∞-Groupoids
  2265. Theorem 62.17 — Eckmann–HiltonTypes as ∞-Groupoids
  2266. Lemma 62.20 — Singletons are contractibleTypes as ∞-Groupoids
  2267. Proposition 62.24 — Equivalences have quasi-inversesTypes as ∞-Groupoids
  2268. Lemma 62.26 — Coherent improvementTypes as ∞-Groupoids
  2269. Theorem 62.27 — Quasi-inverses sufficeTypes as ∞-Groupoids
  2270. Proposition 62.28 — Composition and inversionTypes as ∞-Groupoids
  2271. Lemma 189.30 — Concatenation by a fixed path is an equivalenceTypes as ∞-Groupoids
  2272. Theorem 62.30 — Paths in Σ -typesTypes as ∞-Groupoids
  2273. Lemma 62.31 — Fibrewise equivalences totalizeTypes as ∞-Groupoids
  2274. Proposition 62.32 — Paths in the unit typeTypes as ∞-Groupoids
  2275. Theorem 62.35 — The encode–decode methodTypes as ∞-Groupoids
  2276. Theorem 62.37 — Paths in coproductsTypes as ∞-Groupoids
  2277. Corollary 62.38Types as ∞-Groupoids
  2278. Theorem 62.39 — Paths in the natural numbersTypes as ∞-Groupoids
  2279. Corollary 62.40Types as ∞-Groupoids
  2280. Proposition 189.42 — Natural-number equality is decidableTypes as ∞-Groupoids
  2281. Proposition 189.44 — Natural numbers are a setTypes as ∞-Groupoids
  2282. Lemma 190.3 — Cosimplicial identitiesSimplicial Sets, Horns, and Kan Fibrations
  2283. Lemma 190.4 — Epi–mono factorizationSimplicial Sets, Horns, and Kan Fibrations
  2284. Lemma 190.9 — Yoneda for simplicial setsSimplicial Sets, Horns, and Kan Fibrations
  2285. Lemma 190.12 — Maps out of a horn are matching familiesSimplicial Sets, Horns, and Kan Fibrations
  2286. Proposition 190.14 — Nerves fill inner horns uniquelySimplicial Sets, Horns, and Kan Fibrations
  2287. Proposition 190.15 — Groupoids and outer hornsSimplicial Sets, Horns, and Kan Fibrations
  2288. Proposition 190.17 — Singular complexes are KanSimplicial Sets, Horns, and Kan Fibrations
  2289. Proposition 190.18 — StabilitySimplicial Sets, Horns, and Kan Fibrations
  2290. Proposition 190.21 — Edges in a Kan complexSimplicial Sets, Horns, and Kan Fibrations
  2291. Lemma 65.2 — Calculus of contractibilityUnivalence
  2292. Lemma 65.3 — Coercion is an equivalenceUnivalence
  2293. Theorem 65.7 — ConsistencyUnivalence
  2294. Theorem 65.9 — Transport alongUnivalence
  2295. Proposition 65.10 — Equivalent forms of univalenceUnivalence
  2296. Lemma 65.13 — Fiberwise fibers are retracts of total fibersUnivalence
  2297. Lemma 65.14 — Post-composition with an equivalenceUnivalence
  2298. Lemma 65.15 — Projection of a contractible familyUnivalence
  2299. Theorem 65.16 — Univalence implies weak function extensionalityUnivalence
  2300. Theorem 65.17 — Weak function extensionality implies function extensionalityUnivalence
  2301. Theorem 65.18 — Univalence implies function extensionalityUnivalence
  2302. Lemma 65.19 — Propositionality of the basic predicatesUnivalence
  2303. Corollary 65.20 — Functoriality ofUnivalence
  2304. Lemma 65.21 — Path spaces ofUnivalence
  2305. Theorem 65.22 — Univalence refutes UIPUnivalence
  2306. Corollary 65.23Univalence
  2307. Proposition 193.24 — The two Boolean automorphismsUnivalence
  2308. Lemma 65.27 — Propositions are setsUnivalence
  2309. Lemma 193.29 — Propositionality of being a propositionUnivalence
  2310. Proposition 65.28 — Univalence implies propositional univalenceUnivalence
  2311. Proposition 65.29 — Propositional univalence is weakerUnivalence
  2312. Proposition 65.31 — Failure of canonicityUnivalence
  2313. Lemma 66.5 — Path algebra recollectionsTruncation Levels, Propositions, and Logic
  2314. Lemma 66.6 — Contractibility propagates to pathsTruncation Levels, Propositions, and Logic
  2315. Lemma 66.7 — Pointed propositionsTruncation Levels, Propositions, and Logic
  2316. Lemma 66.8 — Propositions are setsTruncation Levels, Propositions, and Logic
  2317. Theorem 66.9 — The bottom levelsTruncation Levels, Propositions, and Logic
  2318. Theorem 66.10 — CumulativityTruncation Levels, Propositions, and Logic
  2319. Corollary 66.11Truncation Levels, Propositions, and Logic
  2320. Theorem 66.13 — Closure under retractsTruncation Levels, Propositions, and Logic
  2321. Corollary 66.14 — Invariance under equivalenceTruncation Levels, Propositions, and Logic
  2322. Theorem 66.15 — Closure under ΣTruncation Levels, Propositions, and Logic
  2323. Theorem 66.16 — Closure under ΠTruncation Levels, Propositions, and Logic
  2324. Proposition 66.18 — Descent along embeddingsTruncation Levels, Propositions, and Logic
  2325. Lemma 66.19 — Contractible fibers project awayTruncation Levels, Propositions, and Logic
  2326. Lemma 66.20 — Paths in subtypesTruncation Levels, Propositions, and Logic
  2327. Lemma 66.21Truncation Levels, Propositions, and Logic
  2328. Theorem 66.22 — Being truncated is a propositionTruncation Levels, Propositions, and Logic
  2329. Corollary 66.23 — Being an equivalence is a propositionTruncation Levels, Propositions, and Logic
  2330. Theorem 66.25 — The type of n-typesTruncation Levels, Propositions, and Logic
  2331. Lemma 195.26 — Dependent sum over a contractible baseTruncation Levels, Propositions, and Logic
  2332. Theorem 66.26 — UIP and KTruncation Levels, Propositions, and Logic
  2333. Lemma 66.27 — Collapse lemmaTruncation Levels, Propositions, and Logic
  2334. Theorem 66.29 — HedbergTruncation Levels, Propositions, and Logic
  2335. Corollary 66.30Truncation Levels, Propositions, and Logic
  2336. Proposition 66.31 — Separated types are setsTruncation Levels, Propositions, and Logic
  2337. Lemma 66.35Truncation Levels, Propositions, and Logic
  2338. Theorem 66.37 — Universal propertyTruncation Levels, Propositions, and Logic
  2339. Theorem 66.43 — Univalence refutes untruncated excluded middleTruncation Levels, Propositions, and Logic
  2340. Corollary 66.44 — No global double negationTruncation Levels, Propositions, and Logic
  2341. Lemma 66.47 — Equivalent family formTruncation Levels, Propositions, and Logic
  2342. Lemma 66.49 — The type of two-element typesTruncation Levels, Propositions, and Logic
  2343. Theorem 66.50 — No choice for arbitrary typesTruncation Levels, Propositions, and Logic
  2344. Corollary 66.51 — Unique choiceTruncation Levels, Propositions, and Logic
  2345. Theorem 66.54 — Universal propertyTruncation Levels, Propositions, and Logic
  2346. Lemma 66.55Truncation Levels, Propositions, and Logic
  2347. Theorem 66.56 — Path spaces of truncationsTruncation Levels, Propositions, and Logic
  2348. Lemma 66.59Truncation Levels, Propositions, and Logic
  2349. Lemma 66.60 — Extending a central loopTruncation Levels, Propositions, and Logic
  2350. Lemma 66.61 — Automorphisms ofTruncation Levels, Propositions, and Logic
  2351. Theorem 66.62 — Quasi-inversion is not a propositionTruncation Levels, Propositions, and Logic
  2352. Lemma 68.3 — Path-algebra toolkitHigher Inductive Types and Homotopy-Initiality
  2353. Theorem 68.12 — is not trivialHigher Inductive Types and Homotopy-Initiality
  2354. Theorem 68.13 — Universal property of the circleHigher Inductive Types and Homotopy-Initiality
  2355. Theorem 198.16 — Induction and homotopy-initialityHigher Inductive Types and Homotopy-Initiality
  2356. Theorem 68.16Higher Inductive Types and Homotopy-Initiality
  2357. Theorem 68.17 — Function extensionality from the intervalHigher Inductive Types and Homotopy-Initiality
  2358. Theorem 68.20Higher Inductive Types and Homotopy-Initiality
  2359. Theorem 68.23 — Loop–suspension adjunctionHigher Inductive Types and Homotopy-Initiality
  2360. Corollary 68.24Higher Inductive Types and Homotopy-Initiality
  2361. Theorem 68.28 — Universal property of the pushoutHigher Inductive Types and Homotopy-Initiality
  2362. Theorem 68.32Higher Inductive Types and Homotopy-Initiality
  2363. Lemma 68.35Higher Inductive Types and Homotopy-Initiality
  2364. Lemma 68.36 — Induction into setsHigher Inductive Types and Homotopy-Initiality
  2365. Theorem 68.37 — Universal property of set truncationHigher Inductive Types and Homotopy-Initiality
  2366. Lemma 68.39 — Surjectivity of the quotient mapHigher Inductive Types and Homotopy-Initiality
  2367. Theorem 68.40 — Universal property of the set quotientHigher Inductive Types and Homotopy-Initiality
  2368. Theorem 68.41 — EffectivenessHigher Inductive Types and Homotopy-Initiality
  2369. Lemma 68.42 — Canonical representativesHigher Inductive Types and Homotopy-Initiality
  2370. Lemma 198.47 — Internal arithmetic laws used by divisionHigher Inductive Types and Homotopy-Initiality
  2371. Lemma 198.48 — Internal division with remainderHigher Inductive Types and Homotopy-Initiality
  2372. Lemma 198.49 — Division remainder and congruenceHigher Inductive Types and Homotopy-Initiality
  2373. Proposition 69.5 — Group structureCoverings, van Kampen, and the Fundamental Group
  2374. Lemma 69.7 — InterchangeCoverings, van Kampen, and the Fundamental Group
  2375. Theorem 69.8 — Eckmann–HiltonCoverings, van Kampen, and the Fundamental Group
  2376. Corollary 69.9Coverings, van Kampen, and the Fundamental Group
  2377. Lemma 69.10 — Truncation and loop spacesCoverings, van Kampen, and the Fundamental Group
  2378. Corollary 69.11Coverings, van Kampen, and the Fundamental Group
  2379. Proposition 69.13 — Homotopy invarianceCoverings, van Kampen, and the Fundamental Group
  2380. Lemma 69.16 — Integer inductionCoverings, van Kampen, and the Fundamental Group
  2381. Lemma 69.18 — Transport in the coverCoverings, van Kampen, and the Fundamental Group
  2382. Lemma 69.21Coverings, van Kampen, and the Fundamental Group
  2383. Lemma 202.21 — Addition of winding powersCoverings, van Kampen, and the Fundamental Group
  2384. Lemma 69.23Coverings, van Kampen, and the Fundamental Group
  2385. Lemma 69.24Coverings, van Kampen, and the Fundamental Group
  2386. Theorem 69.25 — The fundamental group of the circleCoverings, van Kampen, and the Fundamental Group
  2387. Theorem 202.29 — Coverings of the circleCoverings, van Kampen, and the Fundamental Group
  2388. Corollary 202.30 — Monodromy classificationCoverings, van Kampen, and the Fundamental Group
  2389. Theorem 202.33 — Imported: naive van Kampen; path-space formCoverings, van Kampen, and the Fundamental Group
  2390. Lemma 202.35Coverings, van Kampen, and the Fundamental Group
  2391. Corollary 202.36 — van Kampen for a wedgeCoverings, van Kampen, and the Fundamental Group
  2392. Lemma 74.4Univalent Categories and Rezk Completion
  2393. Lemma 74.8Univalent Categories and Rezk Completion
  2394. Lemma 74.10 — Transport of morphismsUnivalent Categories and Rezk Completion
  2395. Proposition 207.11 — Strict univalent categoriesUnivalent Categories and Rezk Completion
  2396. Proposition 207.13 — The fundamental pregroupoidUnivalent Categories and Rezk Completion
  2397. Lemma 74.14Univalent Categories and Rezk Completion
  2398. Lemma 74.16Univalent Categories and Rezk Completion
  2399. Theorem 74.17 — Functor categoriesUnivalent Categories and Rezk Completion
  2400. Proposition 74.20Univalent Categories and Rezk Completion
  2401. Lemma 74.21 — Unique choice of preimagesUnivalent Categories and Rezk Completion
  2402. Theorem 74.22Univalent Categories and Rezk Completion
  2403. Theorem 74.25 — Equality of precategoriesUnivalent Categories and Rezk Completion
  2404. Lemma 74.26Univalent Categories and Rezk Completion
  2405. Theorem 74.27 — Equality of univalent categoriesUnivalent Categories and Rezk Completion
  2406. Corollary 74.28Univalent Categories and Rezk Completion
  2407. Theorem 74.31 — Yoneda lemmaUnivalent Categories and Rezk Completion
  2408. Corollary 74.32Univalent Categories and Rezk Completion
  2409. Lemma 74.33 — Full subcategoriesUnivalent Categories and Rezk Completion
  2410. Theorem 74.34 — Rezk completionUnivalent Categories and Rezk Completion
  2411. Theorem 74.37 — Universal propertyUnivalent Categories and Rezk Completion
  2412. Theorem 74.40 — Transport of structureUnivalent Categories and Rezk Completion
  2413. Lemma 207.46 — Standard fibers are setsUnivalent Categories and Rezk Completion
  2414. Theorem 74.44 — Structure identity principleUnivalent Categories and Rezk Completion
  2415. Theorem 74.46 — SIP for groupsUnivalent Categories and Rezk Completion
  2416. Lemma 74.49Set-Level Mathematics in Univalent Foundations
  2417. Theorem 74.51 — CantorSet-Level Mathematics in Univalent Foundations
  2418. Theorem 74.52 — Schr"oder–Bernstein; LEMSet-Level Mathematics in Univalent Foundations
  2419. Lemma 74.54Set-Level Mathematics in Univalent Foundations
  2420. Theorem 74.55 — Well-founded inductionSet-Level Mathematics in Univalent Foundations
  2421. Theorem 74.57Set-Level Mathematics in Univalent Foundations
  2422. Lemma 210.12 — Uniqueness of simulationsSet-Level Mathematics in Univalent Foundations
  2423. Theorem 74.59Set-Level Mathematics in Univalent Foundations
  2424. Lemma 74.63Completions and the Real Numbers
  2425. Theorem 211.6 — Dedekind-real additive structureCompletions and the Real Numbers
  2426. Theorem 74.67Completions and the Real Numbers
  2427. Lemma 74.69 — Induction for mere propertiesChoice-Free HII Cauchy Completion
  2428. Theorem 74.70Choice-Free HII Cauchy Completion
  2429. Theorem 74.72 — AgreementChoice-Free HII Cauchy Completion
  2430. Lemma 79.4 — Irrelevance absorbs the missing rulesObservational Equality and Computational Extensionality
  2431. Lemma 79.9 — Transp needs no computation ruleObservational Equality and Computational Extensionality
  2432. Theorem 79.15 — Extensionality, judgmentallyObservational Equality and Computational Extensionality
  2433. Proposition 79.20 — Propositional computation of the derivedObservational Equality and Computational Extensionality
  2434. Theorem 79.26 — Metatheory of TT^ obsObservational Equality and Computational Extensionality
  2435. Theorem 215.28 — Versioned observational-CIC comparisonObservational Equality and Computational Extensionality
  2436. Theorem 79.28 — Impredicative propositionsObservational Equality and Computational Extensionality
  2437. Proposition 79.30 — No equality reflectionObservational Equality and Computational Extensionality
  2438. Proposition 79.31 — Reasoning strength relative to ETTObservational Equality and Computational Extensionality
  2439. Proposition 79.32 — No univalenceObservational Equality and Computational Extensionality
  2440. Proposition 80.2 — Normal form; decidabilityCubical Type Theory I: De Morgan Cubes
  2441. Lemma 80.9 — Judgmental equality yields pathsCubical Type Theory I: De Morgan Cubes
  2442. Lemma 80.16 — Restriction calculusCubical Type Theory I: De Morgan Cubes
  2443. Lemma 80.17 — Quantifier eliminationCubical Type Theory I: De Morgan Cubes
  2444. Theorem 80.28 — Path eliminationCubical Type Theory I: De Morgan Cubes
  2445. Proposition 217.29 — Cubical groupoid lawsCubical Type Theory I: De Morgan Cubes
  2446. Theorem 80.29 — Function extensionality, judgmentalCubical Type Theory I: De Morgan Cubes
  2447. Lemma 80.32 — Contractible types are extensibleCubical Type Theory I: De Morgan Cubes
  2448. Lemma 80.33 — Functions preserve composition up to a pathCubical Type Theory I: De Morgan Cubes
  2449. Lemma 80.34 — Equivalences are fiberwise extensibleCubical Type Theory I: De Morgan Cubes
  2450. Lemma 80.43 — Unglue is an equivalenceCubical Type Theory I: De Morgan Cubes
  2451. Lemma 217.45 — Fiberwise maps over contractible totalsCubical Type Theory I: De Morgan Cubes
  2452. Theorem 80.44 — UnivalenceCubical Type Theory I: De Morgan Cubes
  2453. Proposition 81.10Cubical Type Theory II: Cartesian Cubes and Computation
  2454. Proposition 81.19 — InterderivabilityCubical Type Theory II: Cartesian Cubes and Computation
  2455. Theorem 218.27 — Imported: computational universe paths in C_ ACubical Type Theory II: Cartesian Cubes and Computation
  2456. Theorem 81.29 — Existence and soundnessCubical Type Theory II: Cartesian Cubes and Computation
  2457. Theorem 81.31 — Canonicity for cubical type theoryCubical Type Theory II: Cartesian Cubes and Computation
  2458. Theorem 81.33 — Normalization; Sterling–AngiuliCubical Type Theory II: Cartesian Cubes and Computation
  2459. Corollary 81.34 — DecidabilityCubical Type Theory II: Cartesian Cubes and Computation
  2460. Proposition 1Computational type theory, elaboration, and clause compilation

Search the book

Type to search the local edition.