Lectures onType Theory
Exercises
Scholarly index

Exercises

  1. Exercise 1.1Judgments, Derivations, and Operational Semantics
  2. Exercise 1.2Judgments, Derivations, and Operational Semantics
  3. Exercise 1.3Judgments, Derivations, and Operational Semantics
  4. Exercise 1.4Judgments, Derivations, and Operational Semantics
  5. Exercise 1.5Judgments, Derivations, and Operational Semantics
  6. Exercise 1.6Judgments, Derivations, and Operational Semantics
  7. Exercise 1.7Judgments, Derivations, and Operational Semantics
  8. Exercise 1.8Judgments, Derivations, and Operational Semantics
  9. Exercise 1.9Judgments, Derivations, and Operational Semantics
  10. Exercise 1.10Judgments, Derivations, and Operational Semantics
  11. Exercise 1.11Judgments, Derivations, and Operational Semantics
  12. Exercise 1.12Judgments, Derivations, and Operational Semantics
  13. Exercise 1.13Judgments, Derivations, and Operational Semantics
  14. Exercise 1.14Judgments, Derivations, and Operational Semantics
  15. Exercise 1.15Judgments, Derivations, and Operational Semantics
  16. Exercise 1.16Judgments, Derivations, and Operational Semantics
  17. Exercise 1.17Judgments, Derivations, and Operational Semantics
  18. Exercise 1.18Judgments, Derivations, and Operational Semantics
  19. Exercise 1.19Judgments, Derivations, and Operational Semantics
  20. Exercise 1.20Judgments, Derivations, and Operational Semantics
  21. Exercise 1.20Judgments, Derivations, and Operational Semantics
  22. Exercise 2.1Simple Types, Curry–Howard, Safety, and Normalization
  23. Exercise 2.2Simple Types, Curry–Howard, Safety, and Normalization
  24. Exercise 2.3Simple Types, Curry–Howard, Safety, and Normalization
  25. Exercise 2.4Simple Types, Curry–Howard, Safety, and Normalization
  26. Exercise 2.5Simple Types, Curry–Howard, Safety, and Normalization
  27. Exercise 2.6Simple Types, Curry–Howard, Safety, and Normalization
  28. Exercise 2.7Simple Types, Curry–Howard, Safety, and Normalization
  29. Exercise 2.8Simple Types, Curry–Howard, Safety, and Normalization
  30. Exercise 2.7Simple Types, Curry–Howard, Safety, and Normalization
  31. Exercise 2.8Simple Types, Curry–Howard, Safety, and Normalization
  32. Exercise 2.9Simple Types, Curry–Howard, Safety, and Normalization
  33. Exercise 2.10Simple Types, Curry–Howard, Safety, and Normalization
  34. Exercise 2.11Simple Types, Curry–Howard, Safety, and Normalization
  35. Exercise 2.12Simple Types, Curry–Howard, Safety, and Normalization
  36. Exercise 2.13Simple Types, Curry–Howard, Safety, and Normalization
  37. Exercise 2.15Simple Types, Curry–Howard, Safety, and Normalization
  38. Exercise 2.14Simple Types, Curry–Howard, Safety, and Normalization
  39. Exercise 2.16Simple Types, Curry–Howard, Safety, and Normalization
  40. Exercise 2.17Simple Types, Curry–Howard, Safety, and Normalization
  41. Exercise 2.18Simple Types, Curry–Howard, Safety, and Normalization
  42. Exercise 2.19Simple Types, Curry–Howard, Safety, and Normalization
  43. Exercise 2.22Simple Types, Curry–Howard, Safety, and Normalization
  44. Exercise 3.1First-Order Proof Theory and Sequent Calculi
  45. Exercise 3.2First-Order Proof Theory and Sequent Calculi
  46. Exercise 3.3First-Order Proof Theory and Sequent Calculi
  47. Exercise 3.4First-Order Proof Theory and Sequent Calculi
  48. Exercise 3.5First-Order Proof Theory and Sequent Calculi
  49. Exercise 3.6First-Order Proof Theory and Sequent Calculi
  50. Exercise 3.7First-Order Proof Theory and Sequent Calculi
  51. Exercise 3.8First-Order Proof Theory and Sequent Calculi
  52. Exercise 3.9First-Order Proof Theory and Sequent Calculi
  53. Exercise 3.10First-Order Proof Theory and Sequent Calculi
  54. Exercise 3.1Hindley–Milner Type Inference
  55. Exercise 3.2Hindley–Milner Type Inference
  56. Exercise 3.3Hindley–Milner Type Inference
  57. Exercise 3.4Hindley–Milner Type Inference
  58. Exercise 3.5Hindley–Milner Type Inference
  59. Exercise 3.6Hindley–Milner Type Inference
  60. Exercise 3.7Hindley–Milner Type Inference
  61. Exercise 3.8Hindley–Milner Type Inference
  62. Exercise 3.9Hindley–Milner Type Inference
  63. Exercise 3.10Hindley–Milner Type Inference
  64. Exercise 3.11Hindley–Milner Type Inference
  65. Exercise 3.12Hindley–Milner Type Inference
  66. Exercise 3.13Hindley–Milner Type Inference
  67. Exercise 3.14Hindley–Milner Type Inference
  68. Exercise 3.15Hindley–Milner Type Inference
  69. Exercise 4.16Hindley–Milner Type Inference
  70. Exercise 5.1Semi-Unification and Polymorphic Recursion
  71. Exercise 5.2Semi-Unification and Polymorphic Recursion
  72. Exercise 5.3Semi-Unification and Polymorphic Recursion
  73. Exercise 5.4Semi-Unification and Polymorphic Recursion
  74. Exercise 5.5Semi-Unification and Polymorphic Recursion
  75. Exercise 5.6Semi-Unification and Polymorphic Recursion
  76. Exercise 5.7Semi-Unification and Polymorphic Recursion
  77. Exercise 6.1Dimension Types and Units of Measure
  78. Exercise 6.2Dimension Types and Units of Measure
  79. Exercise 6.3Dimension Types and Units of Measure
  80. Exercise 6.4Dimension Types and Units of Measure
  81. Exercise 6.5Dimension Types and Units of Measure
  82. Exercise 6.6Dimension Types and Units of Measure
  83. Exercise 6.7Dimension Types and Units of Measure
  84. Exercise 6.8Dimension Types and Units of Measure
  85. Exercise 6.9Dimension Types and Units of Measure
  86. Exercise 4.1Row Polymorphism and Extensible Records and Variants
  87. Exercise 4.2Row Polymorphism and Extensible Records and Variants
  88. Exercise 4.3Row Polymorphism and Extensible Records and Variants
  89. Exercise 4.4Row Polymorphism and Extensible Records and Variants
  90. Exercise 4.5Row Polymorphism and Extensible Records and Variants
  91. Exercise 4.6Row Polymorphism and Extensible Records and Variants
  92. Exercise 4.7Row Polymorphism and Extensible Records and Variants
  93. Exercise 4.8Row Polymorphism and Extensible Records and Variants
  94. Exercise 4.10Row Polymorphism and Extensible Records and Variants
  95. Exercise 4.11 — Most-general rows (★ )Row Polymorphism and Extensible Records and Variants
  96. Exercise 4.9Row Polymorphism and Extensible Records and Variants
  97. Exercise 7.12Row Polymorphism and Extensible Records and Variants
  98. Exercise 4.12 — Scoped duplicate records (★ )Row Polymorphism and Extensible Records and Variants
  99. Exercise 4.13 — Ambiguous evidence (★ )Row Polymorphism and Extensible Records and Variants
  100. Exercise 8.1Type-Preserving Compilation of Polymorphic Records
  101. Exercise 8.2Type-Preserving Compilation of Polymorphic Records
  102. Exercise 8.3Type-Preserving Compilation of Polymorphic Records
  103. Exercise 8.4Type-Preserving Compilation of Polymorphic Records
  104. Exercise 8.5Type-Preserving Compilation of Polymorphic Records
  105. Exercise 8.6Type-Preserving Compilation of Polymorphic Records
  106. Exercise 8.7Type-Preserving Compilation of Polymorphic Records
  107. Exercise 8.8Type-Preserving Compilation of Polymorphic Records
  108. Exercise 8.9Type-Preserving Compilation of Polymorphic Records
  109. Exercise 5.1System F, Impredicativity, and Normalization
  110. Exercise 5.2System F, Impredicativity, and Normalization
  111. Exercise 5.3System F, Impredicativity, and Normalization
  112. Exercise 5.4System F, Impredicativity, and Normalization
  113. Exercise 5.5System F, Impredicativity, and Normalization
  114. Exercise 5.6System F, Impredicativity, and Normalization
  115. Exercise 5.7 — *System F, Impredicativity, and Normalization
  116. Exercise 5.8System F, Impredicativity, and Normalization
  117. Exercise 5.9System F, Impredicativity, and Normalization
  118. Exercise 5.10System F, Impredicativity, and Normalization
  119. Exercise 5.11System F, Impredicativity, and Normalization
  120. Exercise 5.13System F, Impredicativity, and Normalization
  121. Exercise 5.12 — *System F, Impredicativity, and Normalization
  122. Exercise 9.14System F, Impredicativity, and Normalization
  123. Exercise 5.14 — *System F, Impredicativity, and Normalization
  124. Exercise 9.15System F, Impredicativity, and Normalization
  125. Exercise 6.1Relational Parametricity and Abstraction Theorems
  126. Exercise 6.2Relational Parametricity and Abstraction Theorems
  127. Exercise 6.3 — *Relational Parametricity and Abstraction Theorems
  128. Exercise 6.4Relational Parametricity and Abstraction Theorems
  129. Exercise 6.5Relational Parametricity and Abstraction Theorems
  130. Exercise 6.6Relational Parametricity and Abstraction Theorems
  131. Exercise 6.7 — *Relational Parametricity and Abstraction Theorems
  132. Exercise 6.8 — *Relational Parametricity and Abstraction Theorems
  133. Exercise 6.9Relational Parametricity and Abstraction Theorems
  134. Exercise 10.10Relational Parametricity and Abstraction Theorems
  135. Exercise 7.1Type Operators, Kinds, and System F-omega
  136. Exercise 7.2Type Operators, Kinds, and System F-omega
  137. Exercise 11.3Type Operators, Kinds, and System F-omega
  138. Exercise 11.4Type Operators, Kinds, and System F-omega
  139. Exercise 11.5Type Operators, Kinds, and System F-omega
  140. Exercise 11.6Type Operators, Kinds, and System F-omega
  141. Exercise 7.5Type Operators, Kinds, and System F-omega
  142. Exercise 7.3Type Operators, Kinds, and System F-omega
  143. Exercise 11.9Type Operators, Kinds, and System F-omega
  144. Exercise 7.4Type Operators, Kinds, and System F-omega
  145. Exercise 7.6Existential Types, Abstract Data, and Representation Independence
  146. Exercise 7.7Existential Types, Abstract Data, and Representation Independence
  147. Exercise 7.8Existential Types, Abstract Data, and Representation Independence
  148. Exercise 7.9Existential Types, Abstract Data, and Representation Independence
  149. Exercise 7.10Existential Types, Abstract Data, and Representation Independence
  150. Exercise 7.11 — *Existential Types, Abstract Data, and Representation Independence
  151. Exercise 7.13Existential Types, Abstract Data, and Representation Independence
  152. Exercise 7.14Existential Types, Abstract Data, and Representation Independence
  153. Exercise 7.20Existential Types, Abstract Data, and Representation Independence
  154. Exercise 12.10Existential Types, Abstract Data, and Representation Independence
  155. Exercise 11.1 — *Qualified Types, Type Classes, and Coherent Dictionary Elaboration
  156. Exercise 11.2Qualified Types, Type Classes, and Coherent Dictionary Elaboration
  157. Exercise 11.3 — *Qualified Types, Type Classes, and Coherent Dictionary Elaboration
  158. Exercise 13.4Qualified Types, Type Classes, and Coherent Dictionary Elaboration
  159. Exercise 13.5Qualified Types, Type Classes, and Coherent Dictionary Elaboration
  160. Exercise 11.5 — *Qualified Types, Type Classes, and Coherent Dictionary Elaboration
  161. Exercise 13.7Qualified Types, Type Classes, and Coherent Dictionary Elaboration
  162. Exercise 11.6 — *Qualified Types, Type Classes, and Coherent Dictionary Elaboration
  163. Exercise 11.7 — *Qualified Types, Type Classes, and Coherent Dictionary Elaboration
  164. Exercise 11.8 — *Qualified Types, Type Classes, and Coherent Dictionary Elaboration
  165. Exercise 12.1ML Modules: Abstraction, Functors, and Sharing
  166. Exercise 12.2ML Modules: Abstraction, Functors, and Sharing
  167. Exercise 12.3ML Modules: Abstraction, Functors, and Sharing
  168. Exercise 12.4ML Modules: Abstraction, Functors, and Sharing
  169. Exercise 12.5ML Modules: Abstraction, Functors, and Sharing
  170. Exercise 12.6ML Modules: Abstraction, Functors, and Sharing
  171. Exercise 12.7ML Modules: Abstraction, Functors, and Sharing
  172. Exercise 14.8ML Modules: Abstraction, Functors, and Sharing
  173. Exercise 12.8ML Modules: Abstraction, Functors, and Sharing
  174. Exercise 12.9ML Modules: Abstraction, Functors, and Sharing
  175. Exercise 12.10ML Modules: Abstraction, Functors, and Sharing
  176. Exercise 12.11ML Modules: Abstraction, Functors, and Sharing
  177. Exercise 12.12ML Modules: Abstraction, Functors, and Sharing
  178. Exercise 15.1 — Merge is functional and commutativeMixML, Recursive Linking, and Definedness
  179. Exercise 15.2 — The missing side conditionMixML, Recursive Linking, and Definedness
  180. Exercise 15.3 — Classify the claimsMixML, Recursive Linking, and Definedness
  181. Exercise 15.4 — A rejected recursive familyMixML, Recursive Linking, and Definedness
  182. Exercise 15.5 — Two notions of completenessMixML, Recursive Linking, and Definedness
  183. Exercise 15.6 — Definedness checkerMixML, Recursive Linking, and Definedness
  184. Exercise 15.7 — A disciplined extensionMixML, Recursive Linking, and Definedness
  185. Exercise 16.1Modular Type Classes and Implicit Modules
  186. Exercise 16.2Modular Type Classes and Implicit Modules
  187. Exercise 16.3Modular Type Classes and Implicit Modules
  188. Exercise 16.4Modular Type Classes and Implicit Modules
  189. Exercise 16.5Modular Type Classes and Implicit Modules
  190. Exercise 16.6Modular Type Classes and Implicit Modules
  191. Exercise 16.7Modular Type Classes and Implicit Modules
  192. Exercise 16.8Modular Type Classes and Implicit Modules
  193. Exercise 16.9Modular Type Classes and Implicit Modules
  194. Exercise 16.10Modular Type Classes and Implicit Modules
  195. Exercise 16.11Modular Type Classes and Implicit Modules
  196. Exercise 16.12Modular Type Classes and Implicit Modules
  197. Exercise 16.13Modular Type Classes and Implicit Modules
  198. Exercise 16.14Modular Type Classes and Implicit Modules
  199. Exercise 16.15Modular Type Classes and Implicit Modules
  200. Exercise 7.16 — *Typed Self-Representation in System F-omega
  201. Exercise 7.17Typed Self-Representation in System F-omega
  202. Exercise 7.18 — *Typed Self-Representation in System F-omega
  203. Exercise 17.4Typed Self-Representation in System F-omega
  204. Exercise 17.5Typed Self-Representation in System F-omega
  205. Exercise 7.19Typed Self-Representation in System F-omega
  206. Exercise 17.7Typed Self-Representation in System F-omega
  207. Exercise 17.8Typed Self-Representation in System F-omega
  208. Exercise 17.9Typed Self-Representation in System F-omega
  209. Exercise 17.10Typed Self-Representation in System F-omega
  210. Exercise 8.1Subtyping, Records, and Bounded Quantification
  211. Exercise 8.2Subtyping, Records, and Bounded Quantification
  212. Exercise 8.3Subtyping, Records, and Bounded Quantification
  213. Exercise 8.4Subtyping, Records, and Bounded Quantification
  214. Exercise 8.5Subtyping, Records, and Bounded Quantification
  215. Exercise 8.6Subtyping, Records, and Bounded Quantification
  216. Exercise 8.7Subtyping, Records, and Bounded Quantification
  217. Exercise 8.8Subtyping, Records, and Bounded Quantification
  218. Exercise 8.9Subtyping, Records, and Bounded Quantification
  219. Exercise 8.10Subtyping, Records, and Bounded Quantification
  220. Exercise 8.11Subtyping, Records, and Bounded Quantification
  221. Exercise 8.12 — *Subtyping, Records, and Bounded Quantification
  222. Exercise 8.13Subtyping, Records, and Bounded Quantification
  223. Exercise 8.14Subtyping, Records, and Bounded Quantification
  224. Exercise 8.15 — *Subtyping, Records, and Bounded Quantification
  225. Exercise 18.16Subtyping, Records, and Bounded Quantification
  226. Exercise 19.1 — Polarity calculationAlgebraic Subtyping and Principal Inference
  227. Exercise 19.2 — Lower-bound eliminationAlgebraic Subtyping and Principal Inference
  228. Exercise 19.3 — A compact principal typeAlgebraic Subtyping and Principal Inference
  229. Exercise 19.4 — Do not transfer the theoremAlgebraic Subtyping and Principal Inference
  230. Exercise 19.5 — Biunification traceAlgebraic Subtyping and Principal Inference
  231. Exercise 19.6 — Why equality loses programsAlgebraic Subtyping and Principal Inference
  232. Exercise 19.7 — Finite polar constraint solverAlgebraic Subtyping and Principal Inference
  233. Exercise 19.8 — A Boolean non-translationAlgebraic Subtyping and Principal Inference
  234. Exercise 9.2Intersection, Union, and Semantic Subtyping
  235. Exercise 9.5Intersection, Union, and Semantic Subtyping
  236. Exercise 9.6Intersection, Union, and Semantic Subtyping
  237. Exercise 9.7Intersection, Union, and Semantic Subtyping
  238. Exercise 9.8Intersection, Union, and Semantic Subtyping
  239. Exercise 9.9 — *Intersection, Union, and Semantic Subtyping
  240. Exercise 9.10Intersection, Union, and Semantic Subtyping
  241. Exercise 9.4Intersection, Union, and Semantic Subtyping
  242. Exercise 9.1Intersection, Union, and Semantic Subtyping
  243. Exercise 9.3Intersection, Union, and Semantic Subtyping
  244. Exercise 9.11Intersection, Union, and Semantic Subtyping
  245. Exercise 9.12Intersection, Union, and Semantic Subtyping
  246. Exercise 9.13Intersection, Union, and Semantic Subtyping
  247. Exercise 9.14Intersection, Union, and Semantic Subtyping
  248. Exercise 9.15Intersection, Union, and Semantic Subtyping
  249. Exercise 20.16Intersection, Union, and Semantic Subtyping
  250. Exercise 9.16Intersection, Union, and Semantic Subtyping
  251. Exercise 9.17Intersection, Union, and Semantic Subtyping
  252. Exercise 20.19Intersection, Union, and Semantic Subtyping
  253. Exercise 21.1Disjoint Intersections, Merge Elaboration, and Coherence
  254. Exercise 21.2Disjoint Intersections, Merge Elaboration, and Coherence
  255. Exercise 21.3Disjoint Intersections, Merge Elaboration, and Coherence
  256. Exercise 21.4Disjoint Intersections, Merge Elaboration, and Coherence
  257. Exercise 21.5Disjoint Intersections, Merge Elaboration, and Coherence
  258. Exercise 21.6Disjoint Intersections, Merge Elaboration, and Coherence
  259. Exercise 21.7Disjoint Intersections, Merge Elaboration, and Coherence
  260. Exercise 21.8Disjoint Intersections, Merge Elaboration, and Coherence
  261. Exercise 21.9Disjoint Intersections, Merge Elaboration, and Coherence
  262. Exercise 10.1Refinement Types and Proof-Carrying Programs
  263. Exercise 10.2Refinement Types and Proof-Carrying Programs
  264. Exercise 10.3Refinement Types and Proof-Carrying Programs
  265. Exercise 10.4Refinement Types and Proof-Carrying Programs
  266. Exercise 10.5Refinement Types and Proof-Carrying Programs
  267. Exercise 10.6Refinement Types and Proof-Carrying Programs
  268. Exercise 10.7Refinement Types and Proof-Carrying Programs
  269. Exercise 10.8Refinement Types and Proof-Carrying Programs
  270. Exercise 10.9Refinement Types and Proof-Carrying Programs
  271. Exercise 10.10Refinement Types and Proof-Carrying Programs
  272. Exercise 22.11Refinement Types and Proof-Carrying Programs
  273. Exercise 23.1Gradual Typing and the Dynamic Boundary
  274. Exercise 23.2Gradual Typing and the Dynamic Boundary
  275. Exercise 23.3Gradual Typing and the Dynamic Boundary
  276. Exercise 23.4Gradual Typing and the Dynamic Boundary
  277. Exercise 23.5Gradual Typing and the Dynamic Boundary
  278. Exercise 23.6Gradual Typing and the Dynamic Boundary
  279. Exercise 23.7Gradual Typing and the Dynamic Boundary
  280. Exercise 23.8Gradual Typing and the Dynamic Boundary
  281. Exercise 23.9Gradual Typing and the Dynamic Boundary
  282. Exercise 23.10Gradual Typing and the Dynamic Boundary
  283. Exercise 23.11Gradual Typing and the Dynamic Boundary
  284. Exercise 23.12Gradual Typing and the Dynamic Boundary
  285. Exercise 23.13Gradual Typing and the Dynamic Boundary
  286. Exercise 23.14Gradual Typing and the Dynamic Boundary
  287. Exercise 23.15Gradual Typing and the Dynamic Boundary
  288. Exercise 24.1Recursive Types, Domains, and General Recursion
  289. Exercise 24.2Recursive Types, Domains, and General Recursion
  290. Exercise 24.3Recursive Types, Domains, and General Recursion
  291. Exercise 24.4Recursive Types, Domains, and General Recursion
  292. Exercise 24.5Recursive Types, Domains, and General Recursion
  293. Exercise 24.6Recursive Types, Domains, and General Recursion
  294. Exercise 24.7Recursive Types, Domains, and General Recursion
  295. Exercise 24.8Recursive Types, Domains, and General Recursion
  296. Exercise 24.9Recursive Types, Domains, and General Recursion
  297. Exercise 24.10Recursive Types, Domains, and General Recursion
  298. Exercise 24.11Recursive Types, Domains, and General Recursion
  299. Exercise 24.12Recursive Types, Domains, and General Recursion
  300. Exercise 24.13Recursive Types, Domains, and General Recursion
  301. Exercise 24.14Recursive Types, Domains, and General Recursion
  302. Exercise 24.15Recursive Types, Domains, and General Recursion
  303. Exercise 24.16Recursive Types, Domains, and General Recursion
  304. Exercise 24.17Recursive Types, Domains, and General Recursion
  305. Exercise 15.1Object Calculi and Recursive Object Types
  306. Exercise 15.2Object Calculi and Recursive Object Types
  307. Exercise 15.3Object Calculi and Recursive Object Types
  308. Exercise 15.4Object Calculi and Recursive Object Types
  309. Exercise 15.5Object Calculi and Recursive Object Types
  310. Exercise 15.6 — *Object Calculi and Recursive Object Types
  311. Exercise 15.7Object Calculi and Recursive Object Types
  312. Exercise 15.8Object Calculi and Recursive Object Types
  313. Exercise 15.9Object Calculi and Recursive Object Types
  314. Exercise 15.10Object Calculi and Recursive Object Types
  315. Exercise 15.11Object Calculi and Recursive Object Types
  316. Exercise 15.12 — *Object Calculi and Recursive Object Types
  317. Exercise 15.13Object Calculi and Recursive Object Types
  318. Exercise 15.14Object Calculi and Recursive Object Types
  319. Exercise 15.15Object Calculi and Recursive Object Types
  320. Exercise 15.16Object Calculi and Recursive Object Types
  321. Exercise 25.17Object Calculi and Recursive Object Types
  322. Exercise 26.1Corrected Inference for Simple Objects
  323. Exercise 26.2Corrected Inference for Simple Objects
  324. Exercise 26.3Corrected Inference for Simple Objects
  325. Exercise 26.4Corrected Inference for Simple Objects
  326. Exercise 26.5Corrected Inference for Simple Objects
  327. Exercise 26.6Corrected Inference for Simple Objects
  328. Exercise 26.7Corrected Inference for Simple Objects
  329. Exercise 26.8Corrected Inference for Simple Objects
  330. Exercise 26.9Corrected Inference for Simple Objects
  331. Exercise 26.10Corrected Inference for Simple Objects
  332. Exercise 16.1OO Self Types, F-Bounds, and Matching
  333. Exercise 16.2OO Self Types, F-Bounds, and Matching
  334. Exercise 16.3OO Self Types, F-Bounds, and Matching
  335. Exercise 16.4OO Self Types, F-Bounds, and Matching
  336. Exercise 16.5OO Self Types, F-Bounds, and Matching
  337. Exercise 16.6OO Self Types, F-Bounds, and Matching
  338. Exercise 16.7OO Self Types, F-Bounds, and Matching
  339. Exercise 16.8OO Self Types, F-Bounds, and Matching
  340. Exercise 16.9OO Self Types, F-Bounds, and Matching
  341. Exercise 16.10OO Self Types, F-Bounds, and Matching
  342. Exercise 16.11OO Self Types, F-Bounds, and Matching
  343. Exercise 16.12OO Self Types, F-Bounds, and Matching
  344. Exercise 16.13OO Self Types, F-Bounds, and Matching
  345. Exercise 16.14OO Self Types, F-Bounds, and Matching
  346. Exercise 21.15OO Self Types, F-Bounds, and Matching
  347. Exercise 22.1Effects, Monads, CBPV, and Algebraic Operations
  348. Exercise 22.2Effects, Monads, CBPV, and Algebraic Operations
  349. Exercise 22.3Effects, Monads, CBPV, and Algebraic Operations
  350. Exercise 22.4Effects, Monads, CBPV, and Algebraic Operations
  351. Exercise 22.5Effects, Monads, CBPV, and Algebraic Operations
  352. Exercise 22.6Effects, Monads, CBPV, and Algebraic Operations
  353. Exercise 22.7Effects, Monads, CBPV, and Algebraic Operations
  354. Exercise 22.8Effects, Monads, CBPV, and Algebraic Operations
  355. Exercise 22.9Effects, Monads, CBPV, and Algebraic Operations
  356. Exercise 22.10Effects, Monads, CBPV, and Algebraic Operations
  357. Exercise 22.11Effects, Monads, CBPV, and Algebraic Operations
  358. Exercise 22.12Effects, Monads, CBPV, and Algebraic Operations
  359. Exercise 22.13Effects, Monads, CBPV, and Algebraic Operations
  360. Exercise 22.14Effects, Monads, CBPV, and Algebraic Operations
  361. Exercise 22.15Effects, Monads, CBPV, and Algebraic Operations
  362. Exercise 22.16Effects, Monads, CBPV, and Algebraic Operations
  363. Exercise 22.17Effects, Monads, CBPV, and Algebraic Operations
  364. Exercise 22.18Effects, Monads, CBPV, and Algebraic Operations
  365. Exercise 22.19Effects, Monads, CBPV, and Algebraic Operations
  366. Exercise 22.20Effects, Monads, CBPV, and Algebraic Operations
  367. Exercise 22.21Effects, Monads, CBPV, and Algebraic Operations
  368. Exercise 23.1Scoped Operations and Explicit Substitution
  369. Exercise 23.2Scoped Operations and Explicit Substitution
  370. Exercise 23.3Scoped Operations and Explicit Substitution
  371. Exercise 23.4Scoped Operations and Explicit Substitution
  372. Exercise 23.5Scoped Operations and Explicit Substitution
  373. Exercise 23.6Scoped Operations and Explicit Substitution
  374. Exercise 23.7Scoped Operations and Explicit Substitution
  375. Exercise 23.8Scoped Operations and Explicit Substitution
  376. Exercise 23.9Scoped Operations and Explicit Substitution
  377. Exercise 23.10Scoped Operations and Explicit Substitution
  378. Exercise 23.11Scoped Operations and Explicit Substitution
  379. Exercise 23.12Scoped Operations and Explicit Substitution
  380. Exercise 23.13Scoped Operations and Explicit Substitution
  381. Exercise 23.14Scoped Operations and Explicit Substitution
  382. Exercise 23.15Scoped Operations and Explicit Substitution
  383. Exercise 24.1 — The opaque-parameter failureHigher-Order Algebraic Effects and Modular Elaboration
  384. Exercise 24.2 — A three-branch operationHigher-Order Algebraic Effects and Modular Elaboration
  385. Exercise 24.3 — The bad bind countedHigher-Order Algebraic Effects and Modular Elaboration
  386. Exercise 24.4 — Functorial actionHigher-Order Algebraic Effects and Modular Elaboration
  387. Exercise 24.5 — Why bind is not this catamorphismHigher-Order Algebraic Effects and Modular Elaboration
  388. Exercise 24.6 — Elaboration of a lifted operationHigher-Order Algebraic Effects and Modular Elaboration
  389. Exercise 24.7 — Continuation after fallbackHigher-Order Algebraic Effects and Modular Elaboration
  390. Exercise 24.8 — Associativity under reassociationHigher-Order Algebraic Effects and Modular Elaboration
  391. Exercise 24.9 — Alternative catch componentHigher-Order Algebraic Effects and Modular Elaboration
  392. Exercise 24.10 — A derived nested-catch lawHigher-Order Algebraic Effects and Modular Elaboration
  393. Exercise 24.11 — Typing versus lawfulnessHigher-Order Algebraic Effects and Modular Elaboration
  394. Exercise 24.12Higher-Order Algebraic Effects and Modular Elaboration
  395. Exercise 24.13Higher-Order Algebraic Effects and Modular Elaboration
  396. Exercise 24.14 — (*)Higher-Order Algebraic Effects and Modular Elaboration
  397. Exercise 24.15 — (*)Higher-Order Algebraic Effects and Modular Elaboration
  398. Exercise 24.16Higher-Order Algebraic Effects and Modular Elaboration
  399. Exercise 24.17Higher-Order Algebraic Effects and Modular Elaboration
  400. Exercise 25.1 — No contractionEffect Rows, Principal Type-and-Effect Inference, and Handlers
  401. Exercise 25.2 — Typing the two catchesEffect Rows, Principal Type-and-Effect Inference, and Handlers
  402. Exercise 25.3 — Forward exactly one layerEffect Rows, Principal Type-and-Effect Inference, and Handlers
  403. Exercise 25.4 — The forwarding caseEffect Rows, Principal Type-and-Effect Inference, and Handlers
  404. Exercise 25.5 — Trace the guardEffect Rows, Principal Type-and-Effect Inference, and Handlers
  405. Exercise 25.6 — Duplicate labels unifyEffect Rows, Principal Type-and-Effect Inference, and Handlers
  406. Exercise 25.7 — W on the transactionEffect Rows, Principal Type-and-Effect Inference, and Handlers
  407. Exercise 25.8 — W on a deep handlerEffect Rows, Principal Type-and-Effect Inference, and Handlers
  408. Exercise 31.9 — Selection and marker provenanceEffect Rows, Principal Type-and-Effect Inference, and Handlers
  409. Exercise 31.10 — A negative row witnessEffect Rows, Principal Type-and-Effect Inference, and Handlers
  410. Exercise 25.9 — The multiplicity boundaryEffect Rows, Principal Type-and-Effect Inference, and Handlers
  411. Exercise 25.10 — Qualified alternativeEffect Rows, Principal Type-and-Effect Inference, and Handlers
  412. Exercise 25.11Effect Rows, Principal Type-and-Effect Inference, and Handlers
  413. Exercise 25.12Effect Rows, Principal Type-and-Effect Inference, and Handlers
  414. Exercise 25.13Effect Rows, Principal Type-and-Effect Inference, and Handlers
  415. Exercise 25.14 — (*)Effect Rows, Principal Type-and-Effect Inference, and Handlers
  416. Exercise 25.15Effect Rows, Principal Type-and-Effect Inference, and Handlers
  417. Exercise 32.1 — Presence is not authorityEffect Capabilities and Tunnelling
  418. Exercise 32.2 — A System Xi derivationEffect Capabilities and Tunnelling
  419. Exercise 32.3 — Locate the restrictionEffect Capabilities and Tunnelling
  420. Exercise 32.4 — The capability caseEffect Capabilities and Tunnelling
  421. Exercise 32.5 — Tracing accidental captureEffect Capabilities and Tunnelling
  422. Exercise 32.6 — Translate one blockEffect Capabilities and Tunnelling
  423. Exercise 32.7 — The tunnelling judgmentEffect Capabilities and Tunnelling
  424. Exercise 32.8 — Two tunneled stepsEffect Capabilities and Tunnelling
  425. Exercise 32.9 — A logical-relation clauseEffect Capabilities and Tunnelling
  426. Exercise 32.10 — Boundary counterexamplesEffect Capabilities and Tunnelling
  427. Exercise 32.11Effect Capabilities and Tunnelling
  428. Exercise 32.12Effect Capabilities and Tunnelling
  429. Exercise 32.13Effect Capabilities and Tunnelling
  430. Exercise 32.14Effect Capabilities and Tunnelling
  431. Exercise 32.15Effect Capabilities and Tunnelling
  432. Exercise 32.16Effect Capabilities and Tunnelling
  433. Exercise 33.1 — Absolute versus relativeModal Effect Types and Source-to-Met Encodings
  434. Exercise 33.2 — Why validity mattersModal Effect Types and Source-to-Met Encodings
  435. Exercise 33.3 — A modal resumptionModal Effect Types and Source-to-Met Encodings
  436. Exercise 33.4 — Translate a row functionModal Effect Types and Source-to-Met Encodings
  437. Exercise 33.5 — Translate a capability blockModal Effect Types and Source-to-Met Encodings
  438. Exercise 33.6 — The handler hypothesisModal Effect Types and Source-to-Met Encodings
  439. Exercise 33.7 — One handler through both encodingsModal Effect Types and Source-to-Met Encodings
  440. Exercise 33.8 — No triangle from a spanModal Effect Types and Source-to-Met Encodings
  441. Exercise 33.9Modal Effect Types and Source-to-Met Encodings
  442. Exercise 33.10Modal Effect Types and Source-to-Met Encodings
  443. Exercise 33.11Modal Effect Types and Source-to-Met Encodings
  444. Exercise 33.12Modal Effect Types and Source-to-Met Encodings
  445. Exercise 33.13Modal Effect Types and Source-to-Met Encodings
  446. Exercise 34.1Lexical Effect Handlers and Direct Compilation
  447. Exercise 34.2Lexical Effect Handlers and Direct Compilation
  448. Exercise 34.3Lexical Effect Handlers and Direct Compilation
  449. Exercise 34.4Lexical Effect Handlers and Direct Compilation
  450. Exercise 34.5Lexical Effect Handlers and Direct Compilation
  451. Exercise 34.6Lexical Effect Handlers and Direct Compilation
  452. Exercise 34.7Lexical Effect Handlers and Direct Compilation
  453. Exercise 34.8Lexical Effect Handlers and Direct Compilation
  454. Exercise 34.9Lexical Effect Handlers and Direct Compilation
  455. Exercise 34.10Lexical Effect Handlers and Direct Compilation
  456. Exercise 34.11Lexical Effect Handlers and Direct Compilation
  457. Exercise 34.12Lexical Effect Handlers and Direct Compilation
  458. Exercise 34.13Lexical Effect Handlers and Direct Compilation
  459. Exercise 35.1Control Operators and Classical Proofs
  460. Exercise 35.2Control Operators and Classical Proofs
  461. Exercise 35.3Control Operators and Classical Proofs
  462. Exercise 35.4Control Operators and Classical Proofs
  463. Exercise 35.5Control Operators and Classical Proofs
  464. Exercise 35.6Control Operators and Classical Proofs
  465. Exercise 35.7Control Operators and Classical Proofs
  466. Exercise 35.8Control Operators and Classical Proofs
  467. Exercise 35.9Control Operators and Classical Proofs
  468. Exercise 35.10Control Operators and Classical Proofs
  469. Exercise 35.11Control Operators and Classical Proofs
  470. Exercise 35.12Control Operators and Classical Proofs
  471. Exercise 35.13Control Operators and Classical Proofs
  472. Exercise 35.14Control Operators and Classical Proofs
  473. Exercise 18.1Linear and Affine Type Systems
  474. Exercise 18.2Linear and Affine Type Systems
  475. Exercise 18.3Linear and Affine Type Systems
  476. Exercise 18.4Linear and Affine Type Systems
  477. Exercise 18.5Linear and Affine Type Systems
  478. Exercise 18.7Linear and Affine Type Systems
  479. Exercise 18.9Linear and Affine Type Systems
  480. Exercise 36.8Linear and Affine Type Systems
  481. Exercise 18.11Linear and Affine Type Systems
  482. Exercise 18.12Linear and Affine Type Systems
  483. Exercise 18.8Linear and Affine Type Systems
  484. Exercise 18.6Linear and Affine Type Systems
  485. Exercise 18.10 — *Linear and Affine Type Systems
  486. Exercise 18.14Linear and Affine Type Systems
  487. Exercise 36.15Linear and Affine Type Systems
  488. Exercise 18.13Linear and Affine Type Systems
  489. Exercise 18.15Linear and Affine Type Systems
  490. Exercise 36.18Linear and Affine Type Systems
  491. Exercise 37.1Evaluation-Strategy Translations
  492. Exercise 37.2Evaluation-Strategy Translations
  493. Exercise 37.3Evaluation-Strategy Translations
  494. Exercise 37.4Evaluation-Strategy Translations
  495. Exercise 37.5Evaluation-Strategy Translations
  496. Exercise 37.6Evaluation-Strategy Translations
  497. Exercise 37.7Evaluation-Strategy Translations
  498. Exercise 37.8Evaluation-Strategy Translations
  499. Exercise 38.1Ordered and Noncommutative Types and the Lambek Calculus
  500. Exercise 38.2Ordered and Noncommutative Types and the Lambek Calculus
  501. Exercise 38.3Ordered and Noncommutative Types and the Lambek Calculus
  502. Exercise 38.4Ordered and Noncommutative Types and the Lambek Calculus
  503. Exercise 38.5Ordered and Noncommutative Types and the Lambek Calculus
  504. Exercise 38.6Ordered and Noncommutative Types and the Lambek Calculus
  505. Exercise 38.7Ordered and Noncommutative Types and the Lambek Calculus
  506. Exercise 38.8Ordered and Noncommutative Types and the Lambek Calculus
  507. Exercise 38.9Ordered and Noncommutative Types and the Lambek Calculus
  508. Exercise 38.10Ordered and Noncommutative Types and the Lambek Calculus
  509. Exercise 38.11Ordered and Noncommutative Types and the Lambek Calculus
  510. Exercise 39.1Polarization, Focusing, and Proof Search
  511. Exercise 39.2Polarization, Focusing, and Proof Search
  512. Exercise 39.3Polarization, Focusing, and Proof Search
  513. Exercise 39.4Polarization, Focusing, and Proof Search
  514. Exercise 39.5Polarization, Focusing, and Proof Search
  515. Exercise 39.6Polarization, Focusing, and Proof Search
  516. Exercise 39.7Polarization, Focusing, and Proof Search
  517. Exercise 39.8Polarization, Focusing, and Proof Search
  518. Exercise 39.9Polarization, Focusing, and Proof Search
  519. Exercise 39.10Polarization, Focusing, and Proof Search
  520. Exercise 39.11Polarization, Focusing, and Proof Search
  521. Exercise 39.12Polarization, Focusing, and Proof Search
  522. Exercise 39.13Polarization, Focusing, and Proof Search
  523. Exercise 40.1Proof Nets, Correctness Criteria, and Cut Elimination
  524. Exercise 40.2Proof Nets, Correctness Criteria, and Cut Elimination
  525. Exercise 40.3Proof Nets, Correctness Criteria, and Cut Elimination
  526. Exercise 40.4Proof Nets, Correctness Criteria, and Cut Elimination
  527. Exercise 40.5Proof Nets, Correctness Criteria, and Cut Elimination
  528. Exercise 40.6Proof Nets, Correctness Criteria, and Cut Elimination
  529. Exercise 40.7Proof Nets, Correctness Criteria, and Cut Elimination
  530. Exercise 40.8Proof Nets, Correctness Criteria, and Cut Elimination
  531. Exercise 40.9Proof Nets, Correctness Criteria, and Cut Elimination
  532. Exercise 40.10Proof Nets, Correctness Criteria, and Cut Elimination
  533. Exercise 40.11Proof Nets, Correctness Criteria, and Cut Elimination
  534. Exercise 40.12Proof Nets, Correctness Criteria, and Cut Elimination
  535. Exercise 40.13Proof Nets, Correctness Criteria, and Cut Elimination
  536. Exercise 41.1Interaction Nets and Interaction Combinators
  537. Exercise 41.2Interaction Nets and Interaction Combinators
  538. Exercise 41.3Interaction Nets and Interaction Combinators
  539. Exercise 41.4Interaction Nets and Interaction Combinators
  540. Exercise 41.5Interaction Nets and Interaction Combinators
  541. Exercise 41.6Interaction Nets and Interaction Combinators
  542. Exercise 41.7Interaction Nets and Interaction Combinators
  543. Exercise 41.8Interaction Nets and Interaction Combinators
  544. Exercise 41.9Interaction Nets and Interaction Combinators
  545. Exercise 41.10Interaction Nets and Interaction Combinators
  546. Exercise 41.11Interaction Nets and Interaction Combinators
  547. Exercise 41.12Interaction Nets and Interaction Combinators
  548. Exercise 41.13Interaction Nets and Interaction Combinators
  549. Exercise 41.14Interaction Nets and Interaction Combinators
  550. Exercise 41.15Interaction Nets and Interaction Combinators
  551. Exercise 41.16Interaction Nets and Interaction Combinators
  552. Exercise 41.17Interaction Nets and Interaction Combinators
  553. Exercise 41.18Interaction Nets and Interaction Combinators
  554. Exercise 42.1Optimal Sharing and Graph Reduction
  555. Exercise 42.2Optimal Sharing and Graph Reduction
  556. Exercise 42.3Optimal Sharing and Graph Reduction
  557. Exercise 42.4Optimal Sharing and Graph Reduction
  558. Exercise 42.5Optimal Sharing and Graph Reduction
  559. Exercise 42.6Optimal Sharing and Graph Reduction
  560. Exercise 42.7Optimal Sharing and Graph Reduction
  561. Exercise 42.8Optimal Sharing and Graph Reduction
  562. Exercise 43.1Bunched Implications and Resource Semantics
  563. Exercise 43.2Bunched Implications and Resource Semantics
  564. Exercise 43.3Bunched Implications and Resource Semantics
  565. Exercise 43.4Bunched Implications and Resource Semantics
  566. Exercise 43.5Bunched Implications and Resource Semantics
  567. Exercise 43.6Bunched Implications and Resource Semantics
  568. Exercise 43.7Bunched Implications and Resource Semantics
  569. Exercise 43.8Bunched Implications and Resource Semantics
  570. Exercise 43.9Bunched Implications and Resource Semantics
  571. Exercise 43.10Bunched Implications and Resource Semantics
  572. Exercise 43.11Bunched Implications and Resource Semantics
  573. Exercise 43.12Bunched Implications and Resource Semantics
  574. Exercise 43.13Bunched Implications and Resource Semantics
  575. Exercise 43.14Bunched Implications and Resource Semantics
  576. Exercise 43.15Bunched Implications and Resource Semantics
  577. Exercise 43.16Bunched Implications and Resource Semantics
  578. Exercise 44.1Separation Logic and Local Reasoning
  579. Exercise 44.2Separation Logic and Local Reasoning
  580. Exercise 44.3Separation Logic and Local Reasoning
  581. Exercise 44.4Separation Logic and Local Reasoning
  582. Exercise 44.5Separation Logic and Local Reasoning
  583. Exercise 44.6Separation Logic and Local Reasoning
  584. Exercise 44.7Separation Logic and Local Reasoning
  585. Exercise 44.8Separation Logic and Local Reasoning
  586. Exercise 44.9Separation Logic and Local Reasoning
  587. Exercise 44.10Separation Logic and Local Reasoning
  588. Exercise 44.11Separation Logic and Local Reasoning
  589. Exercise 44.12Separation Logic and Local Reasoning
  590. Exercise 45.1 — The retrying scheduleConcurrent Separation Logic and Higher-Order Ghost State
  591. Exercise 45.2 — Classifying assertionsConcurrent Separation Logic and Higher-Order Ghost State
  592. Exercise 45.3 — Why the mask shrinksConcurrent Separation Logic and Higher-Order Ghost State
  593. Exercise 45.4 — Simultaneous authority updateConcurrent Separation Logic and Higher-Order Ghost State
  594. Exercise 45.5 — Abort or commitConcurrent Separation Logic and Higher-Order Ghost State
  595. Exercise 45.6 — Read the exact client guaranteeConcurrent Separation Logic and Higher-Order Ghost State
  596. Exercise 45.7 — Reconstructing the atomic proofConcurrent Separation Logic and Higher-Order Ghost State
  597. Exercise 45.8 — A lower-bound clientConcurrent Separation Logic and Higher-Order Ghost State
  598. Exercise 45.9 — Checking the pinned boundaryConcurrent Separation Logic and Higher-Order Ghost State
  599. Exercise 45.10 — The exchanger boundaryConcurrent Separation Logic and Higher-Order Ghost State
  600. Exercise 45.11 — Increment trace checkerConcurrent Separation Logic and Higher-Order Ghost State
  601. Exercise 46.1 — A second shared scopeOwnership, Borrowing, and Affine Resource Protocols
  602. Exercise 46.2 — Exclusive reborrow boundaryOwnership, Borrowing, and Affine Resource Protocols
  603. Exercise 46.3 — A moved handleOwnership, Borrowing, and Affine Resource Protocols
  604. Exercise 46.4 — The Affe region premiseOwnership, Borrowing, and Affine Resource Protocols
  605. Exercise 46.5 — Unique update versus affine useOwnership, Borrowing, and Affine Resource Protocols
  606. Exercise 46.6 — Reclaiming twiceOwnership, Borrowing, and Affine Resource Protocols
  607. Exercise 46.7 — Status-preserving consequencesOwnership, Borrowing, and Affine Resource Protocols
  608. Exercise 46.8 — Bug boundaryOwnership, Borrowing, and Affine Resource Protocols
  609. Exercise 46.9 — Protocol reconstructionOwnership, Borrowing, and Affine Resource Protocols
  610. Exercise 46.10 — Hypothesis boundaryOwnership, Borrowing, and Affine Resource Protocols
  611. Exercise 46.11 — The evidence ledgerOwnership, Borrowing, and Affine Resource Protocols
  612. Exercise 46.12 — Comparing five invariantsOwnership, Borrowing, and Affine Resource Protocols
  613. Exercise 46.13 — Ownership protocol checkerOwnership, Borrowing, and Affine Resource Protocols
  614. Exercise 47.1Uniqueness Types and Destructive Update
  615. Exercise 47.2Uniqueness Types and Destructive Update
  616. Exercise 47.3Uniqueness Types and Destructive Update
  617. Exercise 47.4Uniqueness Types and Destructive Update
  618. Exercise 47.5Uniqueness Types and Destructive Update
  619. Exercise 47.6Uniqueness Types and Destructive Update
  620. Exercise 47.7Uniqueness Types and Destructive Update
  621. Exercise 47.8Uniqueness Types and Destructive Update
  622. Exercise 47.9Uniqueness Types and Destructive Update
  623. Exercise 48.1Place Calculi, Partial Moves, and Field-Sensitive Borrowing
  624. Exercise 48.2Place Calculi, Partial Moves, and Field-Sensitive Borrowing
  625. Exercise 48.3Place Calculi, Partial Moves, and Field-Sensitive Borrowing
  626. Exercise 48.4Place Calculi, Partial Moves, and Field-Sensitive Borrowing
  627. Exercise 48.5Place Calculi, Partial Moves, and Field-Sensitive Borrowing
  628. Exercise 48.6Place Calculi, Partial Moves, and Field-Sensitive Borrowing
  629. Exercise 48.7Place Calculi, Partial Moves, and Field-Sensitive Borrowing
  630. Exercise 48.8Place Calculi, Partial Moves, and Field-Sensitive Borrowing
  631. Exercise 48.9Place Calculi, Partial Moves, and Field-Sensitive Borrowing
  632. Exercise 49.1Mutable Value Semantics and inout Access
  633. Exercise 49.2Mutable Value Semantics and inout Access
  634. Exercise 49.3Mutable Value Semantics and inout Access
  635. Exercise 49.4Mutable Value Semantics and inout Access
  636. Exercise 49.5Mutable Value Semantics and inout Access
  637. Exercise 49.6Mutable Value Semantics and inout Access
  638. Exercise 49.7Mutable Value Semantics and inout Access
  639. Exercise 50.1Capability and Region Types for Typed Memory Management
  640. Exercise 50.2Capability and Region Types for Typed Memory Management
  641. Exercise 50.3Capability and Region Types for Typed Memory Management
  642. Exercise 50.4Capability and Region Types for Typed Memory Management
  643. Exercise 50.5Capability and Region Types for Typed Memory Management
  644. Exercise 50.6Capability and Region Types for Typed Memory Management
  645. Exercise 50.7Capability and Region Types for Typed Memory Management
  646. Exercise 51.1Capture Types and Capture-Set Polymorphism
  647. Exercise 51.2Capture Types and Capture-Set Polymorphism
  648. Exercise 51.3Capture Types and Capture-Set Polymorphism
  649. Exercise 51.4Capture Types and Capture-Set Polymorphism
  650. Exercise 51.5Capture Types and Capture-Set Polymorphism
  651. Exercise 51.6Capture Types and Capture-Set Polymorphism
  652. Exercise 51.7Capture Types and Capture-Set Polymorphism
  653. Exercise 52.1Typestate and State-Transition Protocols
  654. Exercise 52.2Typestate and State-Transition Protocols
  655. Exercise 52.3Typestate and State-Transition Protocols
  656. Exercise 52.4Typestate and State-Transition Protocols
  657. Exercise 52.5Typestate and State-Transition Protocols
  658. Exercise 52.6Typestate and State-Transition Protocols
  659. Exercise 52.7Typestate and State-Transition Protocols
  660. Exercise 53.1Coeffects and Context-Dependent Computation
  661. Exercise 53.2Coeffects and Context-Dependent Computation
  662. Exercise 53.3Coeffects and Context-Dependent Computation
  663. Exercise 53.4Coeffects and Context-Dependent Computation
  664. Exercise 53.5Coeffects and Context-Dependent Computation
  665. Exercise 53.6Coeffects and Context-Dependent Computation
  666. Exercise 53.7Coeffects and Context-Dependent Computation
  667. Exercise 54.1Two Bases for Graded Types: Calculi and Correspondence
  668. Exercise 54.2Two Bases for Graded Types: Calculi and Correspondence
  669. Exercise 54.3Two Bases for Graded Types: Calculi and Correspondence
  670. Exercise 54.4Two Bases for Graded Types: Calculi and Correspondence
  671. Exercise 54.5Two Bases for Graded Types: Calculi and Correspondence
  672. Exercise 54.6Two Bases for Graded Types: Calculi and Correspondence
  673. Exercise 54.7Two Bases for Graded Types: Calculi and Correspondence
  674. Exercise 54.8Two Bases for Graded Types: Calculi and Correspondence
  675. Exercise 54.9Two Bases for Graded Types: Calculi and Correspondence
  676. Exercise 54.10Two Bases for Graded Types: Calculi and Correspondence
  677. Exercise 54.11Two Bases for Graded Types: Calculi and Correspondence
  678. Exercise 54.12Two Bases for Graded Types: Calculi and Correspondence
  679. Exercise 55.1Temporal Types and Functional Reactive Programming
  680. Exercise 55.2Temporal Types and Functional Reactive Programming
  681. Exercise 55.3Temporal Types and Functional Reactive Programming
  682. Exercise 55.4Temporal Types and Functional Reactive Programming
  683. Exercise 55.5Temporal Types and Functional Reactive Programming
  684. Exercise 55.6Temporal Types and Functional Reactive Programming
  685. Exercise 55.7Temporal Types and Functional Reactive Programming
  686. Exercise 55.8Temporal Types and Functional Reactive Programming
  687. Exercise 55.9Temporal Types and Functional Reactive Programming
  688. Exercise 55.10Temporal Types and Functional Reactive Programming
  689. Exercise 56.1Soft Linear Logic and Implicit Complexity
  690. Exercise 56.2Soft Linear Logic and Implicit Complexity
  691. Exercise 56.3Soft Linear Logic and Implicit Complexity
  692. Exercise 56.4Soft Linear Logic and Implicit Complexity
  693. Exercise 56.5Soft Linear Logic and Implicit Complexity
  694. Exercise 56.6Soft Linear Logic and Implicit Complexity
  695. Exercise 56.7Soft Linear Logic and Implicit Complexity
  696. Exercise 56.8Soft Linear Logic and Implicit Complexity
  697. Exercise 56.9Soft Linear Logic and Implicit Complexity
  698. Exercise 56.10Soft Linear Logic and Implicit Complexity
  699. Exercise 56.11Soft Linear Logic and Implicit Complexity
  700. Exercise 57.1Amortized Resource Analysis and Typed Potentials
  701. Exercise 57.2Amortized Resource Analysis and Typed Potentials
  702. Exercise 57.3Amortized Resource Analysis and Typed Potentials
  703. Exercise 57.4Amortized Resource Analysis and Typed Potentials
  704. Exercise 57.5Amortized Resource Analysis and Typed Potentials
  705. Exercise 57.6Amortized Resource Analysis and Typed Potentials
  706. Exercise 57.7Amortized Resource Analysis and Typed Potentials
  707. Exercise 58.1Binary Session Types and Typed Protocols
  708. Exercise 58.2Binary Session Types and Typed Protocols
  709. Exercise 58.3Binary Session Types and Typed Protocols
  710. Exercise 58.4Binary Session Types and Typed Protocols
  711. Exercise 58.5Binary Session Types and Typed Protocols
  712. Exercise 58.6Binary Session Types and Typed Protocols
  713. Exercise 58.7Binary Session Types and Typed Protocols
  714. Exercise 58.8Binary Session Types and Typed Protocols
  715. Exercise 59.1Multiparty and Asynchronous Session Types
  716. Exercise 59.2Multiparty and Asynchronous Session Types
  717. Exercise 59.3Multiparty and Asynchronous Session Types
  718. Exercise 59.4Multiparty and Asynchronous Session Types
  719. Exercise 59.5Multiparty and Asynchronous Session Types
  720. Exercise 59.6Multiparty and Asynchronous Session Types
  721. Exercise 59.7Multiparty and Asynchronous Session Types
  722. Exercise 60.1The Lambda Cube and Pure Type Systems
  723. Exercise 60.2The Lambda Cube and Pure Type Systems
  724. Exercise 60.3The Lambda Cube and Pure Type Systems
  725. Exercise 60.4The Lambda Cube and Pure Type Systems
  726. Exercise 60.5The Lambda Cube and Pure Type Systems
  727. Exercise 60.6The Lambda Cube and Pure Type Systems
  728. Exercise 60.7The Lambda Cube and Pure Type Systems
  729. Exercise 60.8The Lambda Cube and Pure Type Systems
  730. Exercise 60.9The Lambda Cube and Pure Type Systems
  731. Exercise 61.1Logical Frameworks, Encodings, and Adequacy
  732. Exercise 61.2Logical Frameworks, Encodings, and Adequacy
  733. Exercise 61.3Logical Frameworks, Encodings, and Adequacy
  734. Exercise 61.4Logical Frameworks, Encodings, and Adequacy
  735. Exercise 61.5Logical Frameworks, Encodings, and Adequacy
  736. Exercise 61.6Logical Frameworks, Encodings, and Adequacy
  737. Exercise 61.7Logical Frameworks, Encodings, and Adequacy
  738. Exercise 61.8Logical Frameworks, Encodings, and Adequacy
  739. Exercise 62.1Nominal Syntax, Support, and Binding
  740. Exercise 62.2Nominal Syntax, Support, and Binding
  741. Exercise 62.3Nominal Syntax, Support, and Binding
  742. Exercise 62.4Nominal Syntax, Support, and Binding
  743. Exercise 62.5Nominal Syntax, Support, and Binding
  744. Exercise 62.6Nominal Syntax, Support, and Binding
  745. Exercise 63.1Contextual Modal Type Theory and Beluga
  746. Exercise 63.2Contextual Modal Type Theory and Beluga
  747. Exercise 63.3Contextual Modal Type Theory and Beluga
  748. Exercise 63.4Contextual Modal Type Theory and Beluga
  749. Exercise 63.5Contextual Modal Type Theory and Beluga
  750. Exercise 64.1Dependent Nominal Type Theory
  751. Exercise 64.2Dependent Nominal Type Theory
  752. Exercise 64.3Dependent Nominal Type Theory
  753. Exercise 64.4Dependent Nominal Type Theory
  754. Exercise 64.5Dependent Nominal Type Theory
  755. Exercise 64.6Dependent Nominal Type Theory
  756. Exercise 65.1Classical Simple Type Theory and HOL
  757. Exercise 65.2Classical Simple Type Theory and HOL
  758. Exercise 65.3Classical Simple Type Theory and HOL
  759. Exercise 65.4Classical Simple Type Theory and HOL
  760. Exercise 65.5Classical Simple Type Theory and HOL
  761. Exercise 65.6Classical Simple Type Theory and HOL
  762. Exercise 65.7Classical Simple Type Theory and HOL
  763. Exercise 66.1System T and the Dialectica Interpretation
  764. Exercise 66.2System T and the Dialectica Interpretation
  765. Exercise 66.3System T and the Dialectica Interpretation
  766. Exercise 66.4System T and the Dialectica Interpretation
  767. Exercise 66.5System T and the Dialectica Interpretation
  768. Exercise 66.6System T and the Dialectica Interpretation
  769. Exercise 66.7System T and the Dialectica Interpretation
  770. Exercise 67.1Bar Recursion, Choice, and Program Extraction
  771. Exercise 67.2Bar Recursion, Choice, and Program Extraction
  772. Exercise 67.3Bar Recursion, Choice, and Program Extraction
  773. Exercise 67.4Bar Recursion, Choice, and Program Extraction
  774. Exercise 67.5Bar Recursion, Choice, and Program Extraction
  775. Exercise 67.6Bar Recursion, Choice, and Program Extraction
  776. Exercise 67.7Bar Recursion, Choice, and Program Extraction
  777. Exercise 67.8Bar Recursion, Choice, and Program Extraction
  778. Exercise 67.9Bar Recursion, Choice, and Program Extraction
  779. Exercise 68.1Abstract Interpretation, Type Systems, and Verified Static Analysis
  780. Exercise 68.2Abstract Interpretation, Type Systems, and Verified Static Analysis
  781. Exercise 68.3Abstract Interpretation, Type Systems, and Verified Static Analysis
  782. Exercise 68.4Abstract Interpretation, Type Systems, and Verified Static Analysis
  783. Exercise 68.5Abstract Interpretation, Type Systems, and Verified Static Analysis
  784. Exercise 68.6Abstract Interpretation, Type Systems, and Verified Static Analysis
  785. Exercise 68.7Abstract Interpretation, Type Systems, and Verified Static Analysis
  786. Exercise 68.8Abstract Interpretation, Type Systems, and Verified Static Analysis
  787. Exercise 68.9Abstract Interpretation, Type Systems, and Verified Static Analysis
  788. Exercise 68.10Abstract Interpretation, Type Systems, and Verified Static Analysis
  789. Exercise 68.11Abstract Interpretation, Type Systems, and Verified Static Analysis
  790. Exercise 68.12Abstract Interpretation, Type Systems, and Verified Static Analysis
  791. Exercise 68.13Abstract Interpretation, Type Systems, and Verified Static Analysis
  792. Exercise 68.14Abstract Interpretation, Type Systems, and Verified Static Analysis
  793. Exercise 69.1Symbolic Execution, Path Conditions, and Concolic Testing
  794. Exercise 69.2Symbolic Execution, Path Conditions, and Concolic Testing
  795. Exercise 69.3Symbolic Execution, Path Conditions, and Concolic Testing
  796. Exercise 69.4Symbolic Execution, Path Conditions, and Concolic Testing
  797. Exercise 69.5Symbolic Execution, Path Conditions, and Concolic Testing
  798. Exercise 69.6Symbolic Execution, Path Conditions, and Concolic Testing
  799. Exercise 69.7Symbolic Execution, Path Conditions, and Concolic Testing
  800. Exercise 69.8Symbolic Execution, Path Conditions, and Concolic Testing
  801. Exercise 70.1Information-Flow Type Systems and Noninterference
  802. Exercise 70.2Information-Flow Type Systems and Noninterference
  803. Exercise 70.3Information-Flow Type Systems and Noninterference
  804. Exercise 70.4Information-Flow Type Systems and Noninterference
  805. Exercise 70.5Information-Flow Type Systems and Noninterference
  806. Exercise 70.6Information-Flow Type Systems and Noninterference
  807. Exercise 70.7Information-Flow Type Systems and Noninterference
  808. Exercise 70.8Information-Flow Type Systems and Noninterference
  809. Exercise 26.1The Rules of Dependent Type Theory
  810. Exercise 26.2The Rules of Dependent Type Theory
  811. Exercise 26.3The Rules of Dependent Type Theory
  812. Exercise 26.4The Rules of Dependent Type Theory
  813. Exercise 26.5The Rules of Dependent Type Theory
  814. Exercise 26.6The Rules of Dependent Type Theory
  815. Exercise 26.7The Rules of Dependent Type Theory
  816. Exercise 26.8The Rules of Dependent Type Theory
  817. Exercise 26.9The Rules of Dependent Type Theory
  818. Exercise 26.10The Rules of Dependent Type Theory
  819. Exercise 26.11The Rules of Dependent Type Theory
  820. Exercise 26.12The Rules of Dependent Type Theory
  821. Exercise 26.13The Rules of Dependent Type Theory
  822. Exercise 26.14The Rules of Dependent Type Theory
  823. Exercise 26.15The Rules of Dependent Type Theory
  824. Exercise 26.16The Rules of Dependent Type Theory
  825. Exercise 71.17The Rules of Dependent Type Theory
  826. Exercise 71.18The Rules of Dependent Type Theory
  827. Exercise 71.19The Rules of Dependent Type Theory
  828. Exercise 71.20The Rules of Dependent Type Theory
  829. Exercise 27.1Dependent Products, Sums, and Unit
  830. Exercise 27.2Dependent Products, Sums, and Unit
  831. Exercise 27.3Dependent Products, Sums, and Unit
  832. Exercise 27.4Dependent Products, Sums, and Unit
  833. Exercise 27.5Dependent Products, Sums, and Unit
  834. Exercise 27.6Dependent Products, Sums, and Unit
  835. Exercise 27.7Dependent Products, Sums, and Unit
  836. Exercise 27.8Dependent Products, Sums, and Unit
  837. Exercise 27.9Dependent Products, Sums, and Unit
  838. Exercise 27.10Dependent Products, Sums, and Unit
  839. Exercise 27.11Dependent Products, Sums, and Unit
  840. Exercise 27.12Dependent Products, Sums, and Unit
  841. Exercise 27.13Dependent Products, Sums, and Unit
  842. Exercise 27.14Dependent Products, Sums, and Unit
  843. Exercise 27.15Dependent Products, Sums, and Unit
  844. Exercise 27.16Dependent Products, Sums, and Unit
  845. Exercise 27.17Dependent Products, Sums, and Unit
  846. Exercise 27.18Dependent Products, Sums, and Unit
  847. Exercise 27.19Dependent Products, Sums, and Unit
  848. Exercise 72.20Dependent Products, Sums, and Unit
  849. Exercise 72.21Dependent Products, Sums, and Unit
  850. Exercise 72.22Dependent Products, Sums, and Unit
  851. Exercise 72.23Dependent Products, Sums, and Unit
  852. Exercise 28.1Inductive Types
  853. Exercise 28.2Inductive Types
  854. Exercise 28.3Inductive Types
  855. Exercise 28.4Inductive Types
  856. Exercise 28.5Inductive Types
  857. Exercise 28.6Inductive Types
  858. Exercise 28.7Inductive Types
  859. Exercise 28.8Inductive Types
  860. Exercise 28.9Inductive Types
  861. Exercise 28.10Inductive Types
  862. Exercise 28.11Inductive Types
  863. Exercise 28.12Inductive Types
  864. Exercise 28.13Inductive Types
  865. Exercise 28.14Inductive Types
  866. Exercise 28.15Inductive Types
  867. Exercise 28.16Inductive Types
  868. Exercise 28.17Inductive Types
  869. Exercise 28.18Inductive Types
  870. Exercise 28.19Inductive Types
  871. Exercise 28.20Inductive Types
  872. Exercise 28.21Inductive Types
  873. Exercise 28.22Inductive Types
  874. Exercise 28.23Inductive Types
  875. Exercise 73.24Inductive Types
  876. Exercise 73.25Inductive Types
  877. Exercise 73.26Inductive Types
  878. Exercise 73.27Inductive Types
  879. Exercise 73.28Inductive Types
  880. Exercise 73.29Inductive Types
  881. Exercise 73.30Inductive Types
  882. Exercise 29.1Universes and Universe Levels
  883. Exercise 29.2Universes and Universe Levels
  884. Exercise 29.4Universes and Universe Levels
  885. Exercise 29.3Universes and Universe Levels
  886. Exercise 29.8Universes and Universe Levels
  887. Exercise 29.10Universes and Universe Levels
  888. Exercise 29.11Universes and Universe Levels
  889. Exercise 29.12Universes and Universe Levels
  890. Exercise 29.9Universes and Universe Levels
  891. Exercise 29.13Universes and Universe Levels
  892. Exercise 29.14Universes and Universe Levels
  893. Exercise 29.15Universes and Universe Levels
  894. Exercise 74.13Universes and Universe Levels
  895. Exercise 74.14Universes and Universe Levels
  896. Exercise 74.15Universes and Universe Levels
  897. Exercise 74.16Universes and Universe Levels
  898. Exercise 29.5Tarski Universes and Decoding
  899. Exercise 29.6Tarski Universes and Decoding
  900. Exercise 29.7Tarski Universes and Decoding
  901. Exercise 75.4Tarski Universes and Decoding
  902. Exercise 75.5Tarski Universes and Decoding
  903. Exercise 75.6Tarski Universes and Decoding
  904. Exercise 76.1Universe Paradoxes and Hurkens's Construction
  905. Exercise 29.17Universe Paradoxes and Hurkens's Construction
  906. Exercise 76.3Universe Paradoxes and Hurkens's Construction
  907. Exercise 76.4Universe Paradoxes and Hurkens's Construction
  908. Exercise 76.5Universe Paradoxes and Hurkens's Construction
  909. Exercise 30.1Identity Types
  910. Exercise 30.2Identity Types
  911. Exercise 30.3Identity Types
  912. Exercise 30.4Identity Types
  913. Exercise 30.5Identity Types
  914. Exercise 30.6Identity Types
  915. Exercise 30.7Identity Types
  916. Exercise 30.8Identity Types
  917. Exercise 30.9Identity Types
  918. Exercise 30.10Identity Types
  919. Exercise 30.11Identity Types
  920. Exercise 30.12Identity Types
  921. Exercise 30.13Identity Types
  922. Exercise 30.14Identity Types
  923. Exercise 30.15Identity Types
  924. Exercise 77.16Identity Types
  925. Exercise 77.17Identity Types
  926. Exercise 78.1Indexed Inductive Families and Dependent Pattern Matching
  927. Exercise 78.2Indexed Inductive Families and Dependent Pattern Matching
  928. Exercise 78.3Indexed Inductive Families and Dependent Pattern Matching
  929. Exercise 78.4Indexed Inductive Families and Dependent Pattern Matching
  930. Exercise 78.5Indexed Inductive Families and Dependent Pattern Matching
  931. Exercise 78.6Indexed Inductive Families and Dependent Pattern Matching
  932. Exercise 78.7Indexed Inductive Families and Dependent Pattern Matching
  933. Exercise 78.8 — Executable dependent DSLIndexed Inductive Families and Dependent Pattern Matching
  934. Exercise 79.1Dependent Records and Primitive Projections
  935. Exercise 79.2Dependent Records and Primitive Projections
  936. Exercise 79.3Dependent Records and Primitive Projections
  937. Exercise 79.4Dependent Records and Primitive Projections
  938. Exercise 79.5Dependent Records and Primitive Projections
  939. Exercise 79.6Dependent Records and Primitive Projections
  940. Exercise 80.1Universes of Datatype Descriptions and Generic Programs
  941. Exercise 80.2Universes of Datatype Descriptions and Generic Programs
  942. Exercise 80.3Universes of Datatype Descriptions and Generic Programs
  943. Exercise 80.4Universes of Datatype Descriptions and Generic Programs
  944. Exercise 80.5Universes of Datatype Descriptions and Generic Programs
  945. Exercise 80.6Universes of Datatype Descriptions and Generic Programs
  946. Exercise 80.7Universes of Datatype Descriptions and Generic Programs
  947. Exercise 80.8Universes of Datatype Descriptions and Generic Programs
  948. Exercise 80.9Universes of Datatype Descriptions and Generic Programs
  949. Exercise 81.1Containers, Polynomial Functors, and Ornaments
  950. Exercise 81.2Containers, Polynomial Functors, and Ornaments
  951. Exercise 81.3Containers, Polynomial Functors, and Ornaments
  952. Exercise 81.4Containers, Polynomial Functors, and Ornaments
  953. Exercise 81.5Containers, Polynomial Functors, and Ornaments
  954. Exercise 81.6Containers, Polynomial Functors, and Ornaments
  955. Exercise 81.7Containers, Polynomial Functors, and Ornaments
  956. Exercise 81.8Containers, Polynomial Functors, and Ornaments
  957. Exercise 81.9Containers, Polynomial Functors, and Ornaments
  958. Exercise 81.10Containers, Polynomial Functors, and Ornaments
  959. Exercise 81.11Containers, Polynomial Functors, and Ornaments
  960. Exercise 81.12Containers, Polynomial Functors, and Ornaments
  961. Exercise 82.1Well-Founded Recursion
  962. Exercise 82.2Well-Founded Recursion
  963. Exercise 82.3Well-Founded Recursion
  964. Exercise 82.4Well-Founded Recursion
  965. Exercise 82.5Well-Founded Recursion
  966. Exercise 82.6Well-Founded Recursion
  967. Exercise 82.7Well-Founded Recursion
  968. Exercise 83.1Size-Change Termination
  969. Exercise 83.2Size-Change Termination
  970. Exercise 83.3Size-Change Termination
  971. Exercise 83.4Size-Change Termination
  972. Exercise 83.5Size-Change Termination
  973. Exercise 83.6Size-Change Termination
  974. Exercise 83.7Size-Change Termination
  975. Exercise 83.8Size-Change Termination
  976. Exercise 84.1Mendler Recursion, Nested Datatypes, and Mixed Variance
  977. Exercise 84.2Mendler Recursion, Nested Datatypes, and Mixed Variance
  978. Exercise 84.3Mendler Recursion, Nested Datatypes, and Mixed Variance
  979. Exercise 84.4Mendler Recursion, Nested Datatypes, and Mixed Variance
  980. Exercise 84.5Mendler Recursion, Nested Datatypes, and Mixed Variance
  981. Exercise 84.6Mendler Recursion, Nested Datatypes, and Mixed Variance
  982. Exercise 84.7Mendler Recursion, Nested Datatypes, and Mixed Variance
  983. Exercise 84.8Mendler Recursion, Nested Datatypes, and Mixed Variance
  984. Exercise 84.9Mendler Recursion, Nested Datatypes, and Mixed Variance
  985. Exercise 84.10Mendler Recursion, Nested Datatypes, and Mixed Variance
  986. Exercise 85.1Coinduction, Copatterns, and Bisimulation
  987. Exercise 85.2Coinduction, Copatterns, and Bisimulation
  988. Exercise 85.3Coinduction, Copatterns, and Bisimulation
  989. Exercise 85.4Coinduction, Copatterns, and Bisimulation
  990. Exercise 85.5Coinduction, Copatterns, and Bisimulation
  991. Exercise 85.6Coinduction, Copatterns, and Bisimulation
  992. Exercise 85.7Coinduction, Copatterns, and Bisimulation
  993. Exercise 85.8Coinduction, Copatterns, and Bisimulation
  994. Exercise 86.1Recursive Effects and Interaction Trees
  995. Exercise 86.2Recursive Effects and Interaction Trees
  996. Exercise 86.3Recursive Effects and Interaction Trees
  997. Exercise 86.4Recursive Effects and Interaction Trees
  998. Exercise 86.5Recursive Effects and Interaction Trees
  999. Exercise 86.6Recursive Effects and Interaction Trees
  1000. Exercise 86.7Recursive Effects and Interaction Trees
  1001. Exercise 87.1Compositional Linearizability and Modular Concurrent Objects
  1002. Exercise 87.2Compositional Linearizability and Modular Concurrent Objects
  1003. Exercise 87.3Compositional Linearizability and Modular Concurrent Objects
  1004. Exercise 87.4Compositional Linearizability and Modular Concurrent Objects
  1005. Exercise 87.5Compositional Linearizability and Modular Concurrent Objects
  1006. Exercise 87.6Compositional Linearizability and Modular Concurrent Objects
  1007. Exercise 87.7Compositional Linearizability and Modular Concurrent Objects
  1008. Exercise 88.1Possibility Reasoning and Linearizability Hoare Logic
  1009. Exercise 88.2Possibility Reasoning and Linearizability Hoare Logic
  1010. Exercise 88.3Possibility Reasoning and Linearizability Hoare Logic
  1011. Exercise 88.4Possibility Reasoning and Linearizability Hoare Logic
  1012. Exercise 88.5Possibility Reasoning and Linearizability Hoare Logic
  1013. Exercise 88.6Possibility Reasoning and Linearizability Hoare Logic
  1014. Exercise 88.7Possibility Reasoning and Linearizability Hoare Logic
  1015. Exercise 89.1The Calculus of Inductive Constructions
  1016. Exercise 89.2The Calculus of Inductive Constructions
  1017. Exercise 89.3The Calculus of Inductive Constructions
  1018. Exercise 89.4The Calculus of Inductive Constructions
  1019. Exercise 89.5The Calculus of Inductive Constructions
  1020. Exercise 89.6The Calculus of Inductive Constructions
  1021. Exercise 89.7The Calculus of Inductive Constructions
  1022. Exercise 89.8The Calculus of Inductive Constructions
  1023. Exercise 35.1Extensional Type Theory
  1024. Exercise 35.2Extensional Type Theory
  1025. Exercise 35.3Extensional Type Theory
  1026. Exercise 35.4Extensional Type Theory
  1027. Exercise 35.5Extensional Type Theory
  1028. Exercise 35.6Extensional Type Theory
  1029. Exercise 35.7Extensional Type Theory
  1030. Exercise 35.8Extensional Type Theory
  1031. Exercise 35.9Extensional Type Theory
  1032. Exercise 35.10Extensional Type Theory
  1033. Exercise 35.11Extensional Type Theory
  1034. Exercise 35.12Extensional Type Theory
  1035. Exercise 35.13Extensional Type Theory
  1036. Exercise 35.14Extensional Type Theory
  1037. Exercise 35.15Extensional Type Theory
  1038. Exercise 35.16Extensional Type Theory
  1039. Exercise 35.17Extensional Type Theory
  1040. Exercise 35.18Extensional Type Theory
  1041. Exercise 90.19Extensional Type Theory
  1042. Exercise 90.20Extensional Type Theory
  1043. Exercise 91.1Nuprl-Style Computational Type Theory and Realizability
  1044. Exercise 91.2Nuprl-Style Computational Type Theory and Realizability
  1045. Exercise 91.3Nuprl-Style Computational Type Theory and Realizability
  1046. Exercise 91.4Nuprl-Style Computational Type Theory and Realizability
  1047. Exercise 91.5Nuprl-Style Computational Type Theory and Realizability
  1048. Exercise 91.6Nuprl-Style Computational Type Theory and Realizability
  1049. Exercise 91.7Nuprl-Style Computational Type Theory and Realizability
  1050. Exercise 91.8Nuprl-Style Computational Type Theory and Realizability
  1051. Exercise 91.9Nuprl-Style Computational Type Theory and Realizability
  1052. Exercise 91.10Nuprl-Style Computational Type Theory and Realizability
  1053. Exercise 91.11Nuprl-Style Computational Type Theory and Realizability
  1054. Exercise 92.1Logic-Enriched Type Theory and Predicative Mathematics
  1055. Exercise 92.2Logic-Enriched Type Theory and Predicative Mathematics
  1056. Exercise 92.3Logic-Enriched Type Theory and Predicative Mathematics
  1057. Exercise 92.4Logic-Enriched Type Theory and Predicative Mathematics
  1058. Exercise 92.5Logic-Enriched Type Theory and Predicative Mathematics
  1059. Exercise 92.6Logic-Enriched Type Theory and Predicative Mathematics
  1060. Exercise 93.1Dependent Intersections and Same-Subject Refinement
  1061. Exercise 93.2Dependent Intersections and Same-Subject Refinement
  1062. Exercise 93.3Dependent Intersections and Same-Subject Refinement
  1063. Exercise 93.4Dependent Intersections and Same-Subject Refinement
  1064. Exercise 93.5Dependent Intersections and Same-Subject Refinement
  1065. Exercise 93.6Dependent Intersections and Same-Subject Refinement
  1066. Exercise 94.1Subject-Dependent Self Types
  1067. Exercise 94.2Subject-Dependent Self Types
  1068. Exercise 94.3Subject-Dependent Self Types
  1069. Exercise 94.4Subject-Dependent Self Types
  1070. Exercise 94.5Subject-Dependent Self Types
  1071. Exercise 95.1Very Dependent Functions
  1072. Exercise 95.2Very Dependent Functions
  1073. Exercise 95.3Very Dependent Functions
  1074. Exercise 95.4Very Dependent Functions
  1075. Exercise 95.5Very Dependent Functions
  1076. Exercise 95.6Very Dependent Functions
  1077. Exercise 96.1CDLE and Cedille: Lambda-Encoded Induction, Recursion, and Zero-Cost Reuse
  1078. Exercise 96.2CDLE and Cedille: Lambda-Encoded Induction, Recursion, and Zero-Cost Reuse
  1079. Exercise 96.3CDLE and Cedille: Lambda-Encoded Induction, Recursion, and Zero-Cost Reuse
  1080. Exercise 96.4CDLE and Cedille: Lambda-Encoded Induction, Recursion, and Zero-Cost Reuse
  1081. Exercise 96.5CDLE and Cedille: Lambda-Encoded Induction, Recursion, and Zero-Cost Reuse
  1082. Exercise 96.6CDLE and Cedille: Lambda-Encoded Induction, Recursion, and Zero-Cost Reuse
  1083. Exercise 97.1The lambda-Pi-Calculus Modulo Rewriting
  1084. Exercise 97.2The lambda-Pi-Calculus Modulo Rewriting
  1085. Exercise 97.3The lambda-Pi-Calculus Modulo Rewriting
  1086. Exercise 97.4The lambda-Pi-Calculus Modulo Rewriting
  1087. Exercise 97.5The lambda-Pi-Calculus Modulo Rewriting
  1088. Exercise 97.6The lambda-Pi-Calculus Modulo Rewriting
  1089. Exercise 98.1Linear Dependent Type Theory
  1090. Exercise 98.2Linear Dependent Type Theory
  1091. Exercise 98.3Linear Dependent Type Theory
  1092. Exercise 98.4Linear Dependent Type Theory
  1093. Exercise 98.5Linear Dependent Type Theory
  1094. Exercise 98.6Linear Dependent Type Theory
  1095. Exercise 98.7Linear Dependent Type Theory
  1096. Exercise 98.8Linear Dependent Type Theory
  1097. Exercise 99.1Quantitative Dependent Type Theory
  1098. Exercise 99.2Quantitative Dependent Type Theory
  1099. Exercise 99.3Quantitative Dependent Type Theory
  1100. Exercise 99.4Quantitative Dependent Type Theory
  1101. Exercise 99.5Quantitative Dependent Type Theory
  1102. Exercise 99.6Quantitative Dependent Type Theory
  1103. Exercise 99.7Quantitative Dependent Type Theory
  1104. Exercise 100.1Graded Modal Dependent Type Theory
  1105. Exercise 100.2Graded Modal Dependent Type Theory
  1106. Exercise 100.3Graded Modal Dependent Type Theory
  1107. Exercise 100.4Graded Modal Dependent Type Theory
  1108. Exercise 100.5Graded Modal Dependent Type Theory
  1109. Exercise 100.6Graded Modal Dependent Type Theory
  1110. Exercise 100.7Graded Modal Dependent Type Theory
  1111. Exercise 100.8Graded Modal Dependent Type Theory
  1112. Exercise 101.1Graded Erasure and Extraction
  1113. Exercise 101.2Graded Erasure and Extraction
  1114. Exercise 101.3Graded Erasure and Extraction
  1115. Exercise 101.4Graded Erasure and Extraction
  1116. Exercise 101.5Graded Erasure and Extraction
  1117. Exercise 102.1Dependent Session Types and Protocol-Indexed Programming
  1118. Exercise 102.2Dependent Session Types and Protocol-Indexed Programming
  1119. Exercise 102.3Dependent Session Types and Protocol-Indexed Programming
  1120. Exercise 102.4Dependent Session Types and Protocol-Indexed Programming
  1121. Exercise 102.5Dependent Session Types and Protocol-Indexed Programming
  1122. Exercise 102.6Dependent Session Types and Protocol-Indexed Programming
  1123. Exercise 102.7Dependent Session Types and Protocol-Indexed Programming
  1124. Exercise 102.8Dependent Session Types and Protocol-Indexed Programming
  1125. Exercise 103.1Dependent Effects and Call-by-Push-Value
  1126. Exercise 103.2Dependent Effects and Call-by-Push-Value
  1127. Exercise 103.3Dependent Effects and Call-by-Push-Value
  1128. Exercise 103.4Dependent Effects and Call-by-Push-Value
  1129. Exercise 103.5Dependent Effects and Call-by-Push-Value
  1130. Exercise 104.1Weakest Preconditions and Dijkstra Monads
  1131. Exercise 104.2Weakest Preconditions and Dijkstra Monads
  1132. Exercise 104.3Weakest Preconditions and Dijkstra Monads
  1133. Exercise 104.4Weakest Preconditions and Dijkstra Monads
  1134. Exercise 104.5Weakest Preconditions and Dijkstra Monads
  1135. Exercise 105.1Partiality and General Recursion in Dependent Type Theory
  1136. Exercise 105.2Partiality and General Recursion in Dependent Type Theory
  1137. Exercise 105.3Partiality and General Recursion in Dependent Type Theory
  1138. Exercise 105.4Partiality and General Recursion in Dependent Type Theory
  1139. Exercise 105.5Partiality and General Recursion in Dependent Type Theory
  1140. Exercise 105.6Partiality and General Recursion in Dependent Type Theory
  1141. Exercise 106.1Dependent Subtyping, Refinement, and Graduality
  1142. Exercise 106.2Dependent Subtyping, Refinement, and Graduality
  1143. Exercise 106.3Dependent Subtyping, Refinement, and Graduality
  1144. Exercise 106.4Dependent Subtyping, Refinement, and Graduality
  1145. Exercise 106.5Dependent Subtyping, Refinement, and Graduality
  1146. Exercise 106.6Dependent Subtyping, Refinement, and Graduality
  1147. Exercise 106.7Dependent Subtyping, Refinement, and Graduality
  1148. Exercise 106.8Dependent Subtyping, Refinement, and Graduality
  1149. Exercise 107.1Dependent Object Types: Type Members, Bad Bounds, and Recursive Self
  1150. Exercise 107.2Dependent Object Types: Type Members, Bad Bounds, and Recursive Self
  1151. Exercise 107.3Dependent Object Types: Type Members, Bad Bounds, and Recursive Self
  1152. Exercise 107.4Dependent Object Types: Type Members, Bad Bounds, and Recursive Self
  1153. Exercise 107.5Dependent Object Types: Type Members, Bad Bounds, and Recursive Self
  1154. Exercise 107.6Dependent Object Types: Type Members, Bad Bounds, and Recursive Self
  1155. Exercise 107.7Dependent Object Types: Type Members, Bad Bounds, and Recursive Self
  1156. Exercise 107.8Dependent Object Types: Type Members, Bad Bounds, and Recursive Self
  1157. Exercise 108.1Fully Path-Dependent Types: Stable Paths, Singletons, and Modules
  1158. Exercise 108.2Fully Path-Dependent Types: Stable Paths, Singletons, and Modules
  1159. Exercise 108.3Fully Path-Dependent Types: Stable Paths, Singletons, and Modules
  1160. Exercise 108.4Fully Path-Dependent Types: Stable Paths, Singletons, and Modules
  1161. Exercise 108.5Fully Path-Dependent Types: Stable Paths, Singletons, and Modules
  1162. Exercise 108.6Fully Path-Dependent Types: Stable Paths, Singletons, and Modules
  1163. Exercise 108.7Fully Path-Dependent Types: Stable Paths, Singletons, and Modules
  1164. Exercise 108.8Fully Path-Dependent Types: Stable Paths, Singletons, and Modules
  1165. Exercise 108.9Fully Path-Dependent Types: Stable Paths, Singletons, and Modules
  1166. Exercise 109.1Classical Dependent Type Theory and Control
  1167. Exercise 109.2Classical Dependent Type Theory and Control
  1168. Exercise 109.3Classical Dependent Type Theory and Control
  1169. Exercise 109.4Classical Dependent Type Theory and Control
  1170. Exercise 109.5Classical Dependent Type Theory and Control
  1171. Exercise 109.6Classical Dependent Type Theory and Control
  1172. Exercise 109.7Classical Dependent Type Theory and Control
  1173. Exercise 109.8Classical Dependent Type Theory and Control
  1174. Exercise 48.1Trusted Kernels and Bidirectional Checking
  1175. Exercise 48.2Trusted Kernels and Bidirectional Checking
  1176. Exercise 48.3Trusted Kernels and Bidirectional Checking
  1177. Exercise 48.4Trusted Kernels and Bidirectional Checking
  1178. Exercise 48.5Trusted Kernels and Bidirectional Checking
  1179. Exercise 48.6Trusted Kernels and Bidirectional Checking
  1180. Exercise 48.12Trusted Kernels and Bidirectional Checking
  1181. Exercise 48.13Trusted Kernels and Bidirectional Checking
  1182. Exercise 110.9Trusted Kernels and Bidirectional Checking
  1183. Exercise 110.10Trusted Kernels and Bidirectional Checking
  1184. Exercise 49.2Canonicity, Normalization, and Decidable Conversion
  1185. Exercise 49.3Canonicity, Normalization, and Decidable Conversion
  1186. Exercise 49.4Canonicity, Normalization, and Decidable Conversion
  1187. Exercise 49.5Canonicity, Normalization, and Decidable Conversion
  1188. Exercise 49.6Canonicity, Normalization, and Decidable Conversion
  1189. Exercise 49.9Canonicity, Normalization, and Decidable Conversion
  1190. Exercise 49.13Canonicity, Normalization, and Decidable Conversion
  1191. Exercise 49.1Canonicity, Normalization, and Decidable Conversion
  1192. Exercise 49.7Canonicity, Normalization, and Decidable Conversion
  1193. Exercise 49.8Canonicity, Normalization, and Decidable Conversion
  1194. Exercise 49.10Canonicity, Normalization, and Decidable Conversion
  1195. Exercise 49.11Canonicity, Normalization, and Decidable Conversion
  1196. Exercise 49.12Canonicity, Normalization, and Decidable Conversion
  1197. Exercise 49.14Canonicity, Normalization, and Decidable Conversion
  1198. Exercise 49.15Canonicity, Normalization, and Decidable Conversion
  1199. Exercise 111.16Canonicity, Normalization, and Decidable Conversion
  1200. Exercise 111.17Canonicity, Normalization, and Decidable Conversion
  1201. Exercise 112.1Elaboration and Unification
  1202. Exercise 112.2Elaboration and Unification
  1203. Exercise 112.3Elaboration and Unification
  1204. Exercise 112.4Elaboration and Unification
  1205. Exercise 112.5Elaboration and Unification
  1206. Exercise 112.6Elaboration and Unification
  1207. Exercise 112.7Elaboration and Unification
  1208. Exercise 112.8Elaboration and Unification
  1209. Exercise 112.9Elaboration and Unification
  1210. Exercise 112.10Elaboration and Unification
  1211. Exercise 112.11Elaboration and Unification
  1212. Exercise 112.12Elaboration and Unification
  1213. Exercise 112.13Elaboration and Unification
  1214. Exercise 112.14Elaboration and Unification
  1215. Exercise 113.1Efficient First-Order Unification
  1216. Exercise 113.2Efficient First-Order Unification
  1217. Exercise 113.3Efficient First-Order Unification
  1218. Exercise 113.4Efficient First-Order Unification
  1219. Exercise 113.5Efficient First-Order Unification
  1220. Exercise 113.6Efficient First-Order Unification
  1221. Exercise 113.7Efficient First-Order Unification
  1222. Exercise 113.8Efficient First-Order Unification
  1223. Exercise 114.1Proof-Producing Tactics and the Kernel Boundary
  1224. Exercise 114.2Proof-Producing Tactics and the Kernel Boundary
  1225. Exercise 114.3Proof-Producing Tactics and the Kernel Boundary
  1226. Exercise 114.4Proof-Producing Tactics and the Kernel Boundary
  1227. Exercise 115.1Rewriting, Simplification, and Reflection
  1228. Exercise 115.2Rewriting, Simplification, and Reflection
  1229. Exercise 115.3Rewriting, Simplification, and Reflection
  1230. Exercise 115.4Rewriting, Simplification, and Reflection
  1231. Exercise 116.1Typed Metaprogramming and Hygienic Elaboration
  1232. Exercise 116.2Typed Metaprogramming and Hygienic Elaboration
  1233. Exercise 116.3Typed Metaprogramming and Hygienic Elaboration
  1234. Exercise 116.4Typed Metaprogramming and Hygienic Elaboration
  1235. Exercise 117.1First-Class Universe Levels and Level Polymorphism
  1236. Exercise 117.2First-Class Universe Levels and Level Polymorphism
  1237. Exercise 117.3First-Class Universe Levels and Level Polymorphism
  1238. Exercise 117.4First-Class Universe Levels and Level Polymorphism
  1239. Exercise 117.5First-Class Universe Levels and Level Polymorphism
  1240. Exercise 117.6First-Class Universe Levels and Level Polymorphism
  1241. Exercise 118.1Sort Polymorphism and Stratified Type Theory
  1242. Exercise 118.2Sort Polymorphism and Stratified Type Theory
  1243. Exercise 118.3Sort Polymorphism and Stratified Type Theory
  1244. Exercise 118.4Sort Polymorphism and Stratified Type Theory
  1245. Exercise 118.5Sort Polymorphism and Stratified Type Theory
  1246. Exercise 118.6Sort Polymorphism and Stratified Type Theory
  1247. Exercise 118.7Sort Polymorphism and Stratified Type Theory
  1248. Exercise 119.1Coercive Subtyping and Coherent Cast Insertion
  1249. Exercise 119.2Coercive Subtyping and Coherent Cast Insertion
  1250. Exercise 119.3Coercive Subtyping and Coherent Cast Insertion
  1251. Exercise 119.4Coercive Subtyping and Coherent Cast Insertion
  1252. Exercise 119.5Coercive Subtyping and Coherent Cast Insertion
  1253. Exercise 119.6Coercive Subtyping and Coherent Cast Insertion
  1254. Exercise 120.1Definitional Functoriality and Generic Type-Former Action
  1255. Exercise 120.2Definitional Functoriality and Generic Type-Former Action
  1256. Exercise 120.3Definitional Functoriality and Generic Type-Former Action
  1257. Exercise 120.4Definitional Functoriality and Generic Type-Former Action
  1258. Exercise 121.1Compiling Dependent Pattern Matching
  1259. Exercise 121.2Compiling Dependent Pattern Matching
  1260. Exercise 121.3Compiling Dependent Pattern Matching
  1261. Exercise 121.4Compiling Dependent Pattern Matching
  1262. Exercise 121.5Compiling Dependent Pattern Matching
  1263. Exercise 121.6Compiling Dependent Pattern Matching
  1264. Exercise 121.7Compiling Dependent Pattern Matching
  1265. Exercise 121.8Compiling Dependent Pattern Matching
  1266. Exercise 121.9Compiling Dependent Pattern Matching
  1267. Exercise 122.1Datatype Declaration Blocks and Strict Positivity
  1268. Exercise 122.2Datatype Declaration Blocks and Strict Positivity
  1269. Exercise 122.3Datatype Declaration Blocks and Strict Positivity
  1270. Exercise 122.4Datatype Declaration Blocks and Strict Positivity
  1271. Exercise 122.5Datatype Declaration Blocks and Strict Positivity
  1272. Exercise 123.1Recursive Function Groups and Termination
  1273. Exercise 123.2Recursive Function Groups and Termination
  1274. Exercise 123.3Recursive Function Groups and Termination
  1275. Exercise 123.4Recursive Function Groups and Termination
  1276. Exercise 123.5Recursive Function Groups and Termination
  1277. Exercise 124.1Corecursive Definitions, Copatterns, and Productivity
  1278. Exercise 124.2Corecursive Definitions, Copatterns, and Productivity
  1279. Exercise 124.3Corecursive Definitions, Copatterns, and Productivity
  1280. Exercise 124.4Corecursive Definitions, Copatterns, and Productivity
  1281. Exercise 124.5Corecursive Definitions, Copatterns, and Productivity
  1282. Exercise 124.6Corecursive Definitions, Copatterns, and Productivity
  1283. Exercise 125.1Elaborating Dependent Copattern Definitions
  1284. Exercise 125.2Elaborating Dependent Copattern Definitions
  1285. Exercise 125.3Elaborating Dependent Copattern Definitions
  1286. Exercise 125.4Elaborating Dependent Copattern Definitions
  1287. Exercise 125.5Elaborating Dependent Copattern Definitions
  1288. Exercise 126.1Erasure and Execution of Dependent Definitions
  1289. Exercise 126.2Erasure and Execution of Dependent Definitions
  1290. Exercise 126.3Erasure and Execution of Dependent Definitions
  1291. Exercise 126.4Erasure and Execution of Dependent Definitions
  1292. Exercise 126.5Erasure and Execution of Dependent Definitions
  1293. Exercise 126.6Erasure and Execution of Dependent Definitions
  1294. Exercise 126.7Erasure and Execution of Dependent Definitions
  1295. Exercise 126.8Erasure and Execution of Dependent Definitions
  1296. Exercise 126.9Erasure and Execution of Dependent Definitions
  1297. Exercise 127.1Partial Evaluation, Binding-Time Analysis, and the Futamura Projections
  1298. Exercise 127.2Partial Evaluation, Binding-Time Analysis, and the Futamura Projections
  1299. Exercise 127.3Partial Evaluation, Binding-Time Analysis, and the Futamura Projections
  1300. Exercise 127.4Partial Evaluation, Binding-Time Analysis, and the Futamura Projections
  1301. Exercise 127.5Partial Evaluation, Binding-Time Analysis, and the Futamura Projections
  1302. Exercise 127.6Partial Evaluation, Binding-Time Analysis, and the Futamura Projections
  1303. Exercise 127.7Partial Evaluation, Binding-Time Analysis, and the Futamura Projections
  1304. Exercise 127.8Partial Evaluation, Binding-Time Analysis, and the Futamura Projections
  1305. Exercise 127.9Partial Evaluation, Binding-Time Analysis, and the Futamura Projections
  1306. Exercise 128.1Supercompilation, Driving, and Generalization
  1307. Exercise 128.2Supercompilation, Driving, and Generalization
  1308. Exercise 128.3Supercompilation, Driving, and Generalization
  1309. Exercise 128.4Supercompilation, Driving, and Generalization
  1310. Exercise 128.5 — Practical: whistle visualizerSupercompilation, Driving, and Generalization
  1311. Exercise 129.1Typed Multi-Stage Programming and an Evidence-Bounded Interpreter-Tower Case Study
  1312. Exercise 129.2Typed Multi-Stage Programming and an Evidence-Bounded Interpreter-Tower Case Study
  1313. Exercise 129.3Typed Multi-Stage Programming and an Evidence-Bounded Interpreter-Tower Case Study
  1314. Exercise 129.4Typed Multi-Stage Programming and an Evidence-Bounded Interpreter-Tower Case Study
  1315. Exercise 129.5Typed Multi-Stage Programming and an Evidence-Bounded Interpreter-Tower Case Study
  1316. Exercise 129.6Typed Multi-Stage Programming and an Evidence-Bounded Interpreter-Tower Case Study
  1317. Exercise 129.7Typed Multi-Stage Programming and an Evidence-Bounded Interpreter-Tower Case Study
  1318. Exercise 129.8 — Practical: modal stage checkerTyped Multi-Stage Programming and an Evidence-Bounded Interpreter-Tower Case Study
  1319. Exercise 130.1Dependent Multi-Stage Type Theory
  1320. Exercise 130.2Dependent Multi-Stage Type Theory
  1321. Exercise 130.3Dependent Multi-Stage Type Theory
  1322. Exercise 130.4Dependent Multi-Stage Type Theory
  1323. Exercise 130.5Dependent Multi-Stage Type Theory
  1324. Exercise 130.6 — Practical: dependent stage checkerDependent Multi-Stage Type Theory
  1325. Exercise 131.1Explicit Equality Evidence and System FC
  1326. Exercise 131.2Explicit Equality Evidence and System FC
  1327. Exercise 131.3Explicit Equality Evidence and System FC
  1328. Exercise 131.4Explicit Equality Evidence and System FC
  1329. Exercise 131.5Explicit Equality Evidence and System FC
  1330. Exercise 131.6Explicit Equality Evidence and System FC
  1331. Exercise 131.7Explicit Equality Evidence and System FC
  1332. Exercise 131.8Explicit Equality Evidence and System FC
  1333. Exercise 131.9Explicit Equality Evidence and System FC
  1334. Exercise 131.10Explicit Equality Evidence and System FC
  1335. Exercise 131.11 — Practical: coercion kinder and eraserExplicit Equality Evidence and System FC
  1336. Exercise 132.1Systems D and DC: A Dependent Haskell Core Specification
  1337. Exercise 132.2Systems D and DC: A Dependent Haskell Core Specification
  1338. Exercise 132.3Systems D and DC: A Dependent Haskell Core Specification
  1339. Exercise 132.4Systems D and DC: A Dependent Haskell Core Specification
  1340. Exercise 132.5Systems D and DC: A Dependent Haskell Core Specification
  1341. Exercise 132.6Systems D and DC: A Dependent Haskell Core Specification
  1342. Exercise 132.7Systems D and DC: A Dependent Haskell Core Specification
  1343. Exercise 132.8Systems D and DC: A Dependent Haskell Core Specification
  1344. Exercise 132.9 — Practical: relevance and erasure checkerSystems D and DC: A Dependent Haskell Core Specification
  1345. Exercise 133.1Typed Intermediate Languages and Certified Closure Conversion
  1346. Exercise 133.2Typed Intermediate Languages and Certified Closure Conversion
  1347. Exercise 133.3Typed Intermediate Languages and Certified Closure Conversion
  1348. Exercise 133.4Typed Intermediate Languages and Certified Closure Conversion
  1349. Exercise 133.5Typed Intermediate Languages and Certified Closure Conversion
  1350. Exercise 133.6Typed Intermediate Languages and Certified Closure Conversion
  1351. Exercise 133.7 — Practical: type-preserving pipelineTyped Intermediate Languages and Certified Closure Conversion
  1352. Exercise 134.1A Certified Type-Preserving Compiler to Assembly
  1353. Exercise 134.2A Certified Type-Preserving Compiler to Assembly
  1354. Exercise 134.3A Certified Type-Preserving Compiler to Assembly
  1355. Exercise 134.4A Certified Type-Preserving Compiler to Assembly
  1356. Exercise 134.5A Certified Type-Preserving Compiler to Assembly
  1357. Exercise 134.6A Certified Type-Preserving Compiler to Assembly
  1358. Exercise 134.7 — Practical: intrinsic syntax and splicingA Certified Type-Preserving Compiler to Assembly
  1359. Exercise 135.1Defunctionalization, Refunctionalization, and Abstract Machines
  1360. Exercise 135.2Defunctionalization, Refunctionalization, and Abstract Machines
  1361. Exercise 135.3Defunctionalization, Refunctionalization, and Abstract Machines
  1362. Exercise 135.4Defunctionalization, Refunctionalization, and Abstract Machines
  1363. Exercise 135.5Defunctionalization, Refunctionalization, and Abstract Machines
  1364. Exercise 135.6Defunctionalization, Refunctionalization, and Abstract Machines
  1365. Exercise 135.7Defunctionalization, Refunctionalization, and Abstract Machines
  1366. Exercise 135.8 — Practical: derive the machineDefunctionalization, Refunctionalization, and Abstract Machines
  1367. Exercise 136.1Secure Compilation and Robust Property Preservation
  1368. Exercise 136.2Secure Compilation and Robust Property Preservation
  1369. Exercise 136.3Secure Compilation and Robust Property Preservation
  1370. Exercise 136.4Secure Compilation and Robust Property Preservation
  1371. Exercise 136.5Secure Compilation and Robust Property Preservation
  1372. Exercise 136.6Secure Compilation and Robust Property Preservation
  1373. Exercise 136.7Secure Compilation and Robust Property Preservation
  1374. Exercise 136.8 — Practical: criteria checkerSecure Compilation and Robust Property Preservation
  1375. Exercise 137.1Dependent Closure Conversion for the Calculus of Constructions
  1376. Exercise 137.2Dependent Closure Conversion for the Calculus of Constructions
  1377. Exercise 137.3Dependent Closure Conversion for the Calculus of Constructions
  1378. Exercise 137.4Dependent Closure Conversion for the Calculus of Constructions
  1379. Exercise 137.5Dependent Closure Conversion for the Calculus of Constructions
  1380. Exercise 137.6Dependent Closure Conversion for the Calculus of Constructions
  1381. Exercise 137.7 — Practical: closure conversion checkerDependent Closure Conversion for the Calculus of Constructions
  1382. Exercise 138.1Dependency-Preserving A-Normal Form
  1383. Exercise 138.2Dependency-Preserving A-Normal Form
  1384. Exercise 138.3Dependency-Preserving A-Normal Form
  1385. Exercise 138.4Dependency-Preserving A-Normal Form
  1386. Exercise 138.5Dependency-Preserving A-Normal Form
  1387. Exercise 138.6Dependency-Preserving A-Normal Form
  1388. Exercise 138.7Dependency-Preserving A-Normal Form
  1389. Exercise 138.8 — Practical: ANF translator and checkerDependency-Preserving A-Normal Form
  1390. Exercise 139.1Typed Functional Array Languages: Shapes, Uniqueness, and Parallel Compilation
  1391. Exercise 139.2Typed Functional Array Languages: Shapes, Uniqueness, and Parallel Compilation
  1392. Exercise 139.3Typed Functional Array Languages: Shapes, Uniqueness, and Parallel Compilation
  1393. Exercise 139.4Typed Functional Array Languages: Shapes, Uniqueness, and Parallel Compilation
  1394. Exercise 139.5Typed Functional Array Languages: Shapes, Uniqueness, and Parallel Compilation
  1395. Exercise 139.6Typed Functional Array Languages: Shapes, Uniqueness, and Parallel Compilation
  1396. Exercise 139.7Typed Functional Array Languages: Shapes, Uniqueness, and Parallel Compilation
  1397. Exercise 139.8Typed Functional Array Languages: Shapes, Uniqueness, and Parallel Compilation
  1398. Exercise 139.9 — Practical: size-dependent checker and evaluatorTyped Functional Array Languages: Shapes, Uniqueness, and Parallel Compilation
  1399. Exercise 140.1Verified Metatheory and Realistic Trusted Kernels
  1400. Exercise 140.2Verified Metatheory and Realistic Trusted Kernels
  1401. Exercise 140.3Verified Metatheory and Realistic Trusted Kernels
  1402. Exercise 140.4Verified Metatheory and Realistic Trusted Kernels
  1403. Exercise 140.5Verified Metatheory and Realistic Trusted Kernels
  1404. Exercise 140.6Verified Metatheory and Realistic Trusted Kernels
  1405. Exercise 140.7 — Practical: a declaration and erasure traceVerified Metatheory and Realistic Trusted Kernels
  1406. Exercise 141.1Categories, Functors, and Representability
  1407. Exercise 141.2Categories, Functors, and Representability
  1408. Exercise 141.3Categories, Functors, and Representability
  1409. Exercise 141.4Categories, Functors, and Representability
  1410. Exercise 141.5Categories, Functors, and Representability
  1411. Exercise 141.6Categories, Functors, and Representability
  1412. Exercise 141.7Categories, Functors, and Representability
  1413. Exercise 141.8Categories, Functors, and Representability
  1414. Exercise 141.9Categories, Functors, and Representability
  1415. Exercise 141.10Categories, Functors, and Representability
  1416. Exercise 141.11Categories, Functors, and Representability
  1417. Exercise 141.12Categories, Functors, and Representability
  1418. Exercise 141.13Categories, Functors, and Representability
  1419. Exercise 141.14Categories, Functors, and Representability
  1420. Exercise 141.15Categories, Functors, and Representability
  1421. Exercise 141.16Categories, Functors, and Representability
  1422. Exercise 141.17Categories, Functors, and Representability
  1423. Exercise 141.18Categories, Functors, and Representability
  1424. Exercise 141.19Categories, Functors, and Representability
  1425. Exercise 141.20Categories, Functors, and Representability
  1426. Exercise 141.21Categories, Functors, and Representability
  1427. Exercise 141.22Categories, Functors, and Representability
  1428. Exercise 141.23Categories, Functors, and Representability
  1429. Exercise 142.1Adjunctions, Limits, and Locally Cartesian Closure
  1430. Exercise 142.2Adjunctions, Limits, and Locally Cartesian Closure
  1431. Exercise 142.3Adjunctions, Limits, and Locally Cartesian Closure
  1432. Exercise 142.4Adjunctions, Limits, and Locally Cartesian Closure
  1433. Exercise 142.5Adjunctions, Limits, and Locally Cartesian Closure
  1434. Exercise 142.6Adjunctions, Limits, and Locally Cartesian Closure
  1435. Exercise 142.7Adjunctions, Limits, and Locally Cartesian Closure
  1436. Exercise 142.8Adjunctions, Limits, and Locally Cartesian Closure
  1437. Exercise 142.9Adjunctions, Limits, and Locally Cartesian Closure
  1438. Exercise 142.10Adjunctions, Limits, and Locally Cartesian Closure
  1439. Exercise 142.11Adjunctions, Limits, and Locally Cartesian Closure
  1440. Exercise 142.12Adjunctions, Limits, and Locally Cartesian Closure
  1441. Exercise 142.13Adjunctions, Limits, and Locally Cartesian Closure
  1442. Exercise 142.14Adjunctions, Limits, and Locally Cartesian Closure
  1443. Exercise 142.15Adjunctions, Limits, and Locally Cartesian Closure
  1444. Exercise 142.16Adjunctions, Limits, and Locally Cartesian Closure
  1445. Exercise 142.17Adjunctions, Limits, and Locally Cartesian Closure
  1446. Exercise 142.18Adjunctions, Limits, and Locally Cartesian Closure
  1447. Exercise 142.19Adjunctions, Limits, and Locally Cartesian Closure
  1448. Exercise 142.20Adjunctions, Limits, and Locally Cartesian Closure
  1449. Exercise 142.21Adjunctions, Limits, and Locally Cartesian Closure
  1450. Exercise 142.22Adjunctions, Limits, and Locally Cartesian Closure
  1451. Exercise 142.23Adjunctions, Limits, and Locally Cartesian Closure
  1452. Exercise 142.24Adjunctions, Limits, and Locally Cartesian Closure
  1453. Exercise 142.25Adjunctions, Limits, and Locally Cartesian Closure
  1454. Exercise 142.26Adjunctions, Limits, and Locally Cartesian Closure
  1455. Exercise 142.27Adjunctions, Limits, and Locally Cartesian Closure
  1456. Exercise 143.1Categorical Logic, Hyperdoctrines, and Internal Languages
  1457. Exercise 143.2Categorical Logic, Hyperdoctrines, and Internal Languages
  1458. Exercise 143.3Categorical Logic, Hyperdoctrines, and Internal Languages
  1459. Exercise 143.4Categorical Logic, Hyperdoctrines, and Internal Languages
  1460. Exercise 143.5Categorical Logic, Hyperdoctrines, and Internal Languages
  1461. Exercise 143.6Categorical Logic, Hyperdoctrines, and Internal Languages
  1462. Exercise 143.7Categorical Logic, Hyperdoctrines, and Internal Languages
  1463. Exercise 143.8Categorical Logic, Hyperdoctrines, and Internal Languages
  1464. Exercise 143.9Categorical Logic, Hyperdoctrines, and Internal Languages
  1465. Exercise 143.10Categorical Logic, Hyperdoctrines, and Internal Languages
  1466. Exercise 143.11Categorical Logic, Hyperdoctrines, and Internal Languages
  1467. Exercise 143.12Categorical Logic, Hyperdoctrines, and Internal Languages
  1468. Exercise 143.13Categorical Logic, Hyperdoctrines, and Internal Languages
  1469. Exercise 144.1Triposes, Toposes, and Realizability
  1470. Exercise 144.2Triposes, Toposes, and Realizability
  1471. Exercise 144.3Triposes, Toposes, and Realizability
  1472. Exercise 144.4Triposes, Toposes, and Realizability
  1473. Exercise 144.5Triposes, Toposes, and Realizability
  1474. Exercise 144.6Triposes, Toposes, and Realizability
  1475. Exercise 144.7Triposes, Toposes, and Realizability
  1476. Exercise 144.8Triposes, Toposes, and Realizability
  1477. Exercise 144.9Triposes, Toposes, and Realizability
  1478. Exercise 144.10Triposes, Toposes, and Realizability
  1479. Exercise 145.1Classical Realizability, Poles, and Orthogonality
  1480. Exercise 145.2Classical Realizability, Poles, and Orthogonality
  1481. Exercise 145.3Classical Realizability, Poles, and Orthogonality
  1482. Exercise 145.4Classical Realizability, Poles, and Orthogonality
  1483. Exercise 145.5Classical Realizability, Poles, and Orthogonality
  1484. Exercise 145.6Classical Realizability, Poles, and Orthogonality
  1485. Exercise 145.7Classical Realizability, Poles, and Orthogonality
  1486. Exercise 145.8Classical Realizability, Poles, and Orthogonality
  1487. Exercise 145.9Classical Realizability, Poles, and Orthogonality
  1488. Exercise 145.10Classical Realizability, Poles, and Orthogonality
  1489. Exercise 145.11Classical Realizability, Poles, and Orthogonality
  1490. Exercise 54.1Algebraic Syntax, CwFs, and Initiality
  1491. Exercise 54.2Algebraic Syntax, CwFs, and Initiality
  1492. Exercise 54.3Algebraic Syntax, CwFs, and Initiality
  1493. Exercise 54.4Algebraic Syntax, CwFs, and Initiality
  1494. Exercise 54.5Algebraic Syntax, CwFs, and Initiality
  1495. Exercise 54.6Algebraic Syntax, CwFs, and Initiality
  1496. Exercise 54.7Algebraic Syntax, CwFs, and Initiality
  1497. Exercise 54.8Algebraic Syntax, CwFs, and Initiality
  1498. Exercise 54.9Algebraic Syntax, CwFs, and Initiality
  1499. Exercise 54.10Algebraic Syntax, CwFs, and Initiality
  1500. Exercise 54.11Algebraic Syntax, CwFs, and Initiality
  1501. Exercise 54.12Algebraic Syntax, CwFs, and Initiality
  1502. Exercise 54.13Algebraic Syntax, CwFs, and Initiality
  1503. Exercise 54.14Algebraic Syntax, CwFs, and Initiality
  1504. Exercise 54.15Algebraic Syntax, CwFs, and Initiality
  1505. Exercise 54.16Algebraic Syntax, CwFs, and Initiality
  1506. Exercise 54.17Algebraic Syntax, CwFs, and Initiality
  1507. Exercise 54.18Algebraic Syntax, CwFs, and Initiality
  1508. Exercise 54.19Algebraic Syntax, CwFs, and Initiality
  1509. Exercise 116.20Algebraic Syntax, CwFs, and Initiality
  1510. Exercise 116.21Algebraic Syntax, CwFs, and Initiality
  1511. Exercise 147.1Generalized Algebraic Theories
  1512. Exercise 147.2Generalized Algebraic Theories
  1513. Exercise 147.3Generalized Algebraic Theories
  1514. Exercise 147.4Generalized Algebraic Theories
  1515. Exercise 147.5Generalized Algebraic Theories
  1516. Exercise 147.6Generalized Algebraic Theories
  1517. Exercise 147.7Generalized Algebraic Theories
  1518. Exercise 147.8Generalized Algebraic Theories
  1519. Exercise 147.9Generalized Algebraic Theories
  1520. Exercise 147.10Generalized Algebraic Theories
  1521. Exercise 147.11Generalized Algebraic Theories
  1522. Exercise 147.12Generalized Algebraic Theories
  1523. Exercise 148.1Explicit-Substitution Calculi
  1524. Exercise 148.2Explicit-Substitution Calculi
  1525. Exercise 148.3Explicit-Substitution Calculi
  1526. Exercise 148.4Explicit-Substitution Calculi
  1527. Exercise 148.5Explicit-Substitution Calculi
  1528. Exercise 148.6Explicit-Substitution Calculi
  1529. Exercise 148.7Explicit-Substitution Calculi
  1530. Exercise 148.8Explicit-Substitution Calculi
  1531. Exercise 148.9Explicit-Substitution Calculi
  1532. Exercise 148.10Explicit-Substitution Calculi
  1533. Exercise 148.11Explicit-Substitution Calculi
  1534. Exercise 149.1Categorical Semantics of Scoped Operations
  1535. Exercise 149.2Categorical Semantics of Scoped Operations
  1536. Exercise 149.3Categorical Semantics of Scoped Operations
  1537. Exercise 149.4Categorical Semantics of Scoped Operations
  1538. Exercise 149.5Categorical Semantics of Scoped Operations
  1539. Exercise 149.6Categorical Semantics of Scoped Operations
  1540. Exercise 149.7Categorical Semantics of Scoped Operations
  1541. Exercise 150.1Categorical Semantics of Coeffects
  1542. Exercise 150.2Categorical Semantics of Coeffects
  1543. Exercise 150.3Categorical Semantics of Coeffects
  1544. Exercise 150.4Categorical Semantics of Coeffects
  1545. Exercise 150.5Categorical Semantics of Coeffects
  1546. Exercise 150.6Categorical Semantics of Coeffects
  1547. Exercise 150.7Categorical Semantics of Coeffects
  1548. Exercise 151.1Set and CwF Models of Type Theory
  1549. Exercise 151.2Set and CwF Models of Type Theory
  1550. Exercise 151.3Set and CwF Models of Type Theory
  1551. Exercise 151.4Set and CwF Models of Type Theory
  1552. Exercise 151.5Set and CwF Models of Type Theory
  1553. Exercise 151.6Set and CwF Models of Type Theory
  1554. Exercise 151.7Set and CwF Models of Type Theory
  1555. Exercise 151.8Set and CwF Models of Type Theory
  1556. Exercise 151.9Set and CwF Models of Type Theory
  1557. Exercise 151.10Set and CwF Models of Type Theory
  1558. Exercise 151.11Set and CwF Models of Type Theory
  1559. Exercise 151.12Set and CwF Models of Type Theory
  1560. Exercise 151.13Set and CwF Models of Type Theory
  1561. Exercise 151.14Set and CwF Models of Type Theory
  1562. Exercise 151.15Set and CwF Models of Type Theory
  1563. Exercise 151.16 — Practical: a set-model evaluatorSet and CwF Models of Type Theory
  1564. Exercise 152.1Groupoid and Path-Object Models of Intensional Type Theory
  1565. Exercise 152.2Groupoid and Path-Object Models of Intensional Type Theory
  1566. Exercise 152.3Groupoid and Path-Object Models of Intensional Type Theory
  1567. Exercise 152.4Groupoid and Path-Object Models of Intensional Type Theory
  1568. Exercise 152.5Groupoid and Path-Object Models of Intensional Type Theory
  1569. Exercise 152.6Groupoid and Path-Object Models of Intensional Type Theory
  1570. Exercise 152.7Groupoid and Path-Object Models of Intensional Type Theory
  1571. Exercise 152.8 — Practical: a finite groupoid model checkerGroupoid and Path-Object Models of Intensional Type Theory
  1572. Exercise 153.1Setoid and PER Models of Type Theory
  1573. Exercise 153.2Setoid and PER Models of Type Theory
  1574. Exercise 153.3Setoid and PER Models of Type Theory
  1575. Exercise 153.4Setoid and PER Models of Type Theory
  1576. Exercise 153.5Setoid and PER Models of Type Theory
  1577. Exercise 153.6Setoid and PER Models of Type Theory
  1578. Exercise 153.7 — Practical: a finite setoid model checkerSetoid and PER Models of Type Theory
  1579. Exercise 154.1Recursive Domain Semantics and Computational Adequacy
  1580. Exercise 154.2Recursive Domain Semantics and Computational Adequacy
  1581. Exercise 154.3Recursive Domain Semantics and Computational Adequacy
  1582. Exercise 154.4Recursive Domain Semantics and Computational Adequacy
  1583. Exercise 154.5Recursive Domain Semantics and Computational Adequacy
  1584. Exercise 154.6Recursive Domain Semantics and Computational Adequacy
  1585. Exercise 154.7 — Practical: an effect-tree evaluatorRecursive Domain Semantics and Computational Adequacy
  1586. Exercise 155.1Dependent PER-Enriched Domain Models
  1587. Exercise 155.2Dependent PER-Enriched Domain Models
  1588. Exercise 155.3Dependent PER-Enriched Domain Models
  1589. Exercise 155.4Dependent PER-Enriched Domain Models
  1590. Exercise 155.5Dependent PER-Enriched Domain Models
  1591. Exercise 155.6Dependent PER-Enriched Domain Models
  1592. Exercise 155.7 — Practical: a complete-monotone PER checkerDependent PER-Enriched Domain Models
  1593. Exercise 156.1Coherence and Local Universes
  1594. Exercise 156.2Coherence and Local Universes
  1595. Exercise 156.3Coherence and Local Universes
  1596. Exercise 156.4Coherence and Local Universes
  1597. Exercise 156.5Coherence and Local Universes
  1598. Exercise 156.6Coherence and Local Universes
  1599. Exercise 156.7Coherence and Local Universes
  1600. Exercise 156.8 — Practical: a strictness checkerCoherence and Local Universes
  1601. Exercise 157.1Games, Arenas, and Strategies
  1602. Exercise 157.2Games, Arenas, and Strategies
  1603. Exercise 157.3Games, Arenas, and Strategies
  1604. Exercise 157.4Games, Arenas, and Strategies
  1605. Exercise 157.5Games, Arenas, and Strategies
  1606. Exercise 157.6Games, Arenas, and Strategies
  1607. Exercise 157.7Games, Arenas, and Strategies
  1608. Exercise 157.8 — Practical: a strategy interpreterGames, Arenas, and Strategies
  1609. Exercise 158.1Definability and Full Abstraction for PCF
  1610. Exercise 158.2Definability and Full Abstraction for PCF
  1611. Exercise 158.3Definability and Full Abstraction for PCF
  1612. Exercise 158.4Definability and Full Abstraction for PCF
  1613. Exercise 158.5Definability and Full Abstraction for PCF
  1614. Exercise 158.6Definability and Full Abstraction for PCF
  1615. Exercise 158.7 — Practical: a definability compilerDefinability and Full Abstraction for PCF
  1616. Exercise 159.1Symmetric Monoidal Categories and Graphical Linear Semantics
  1617. Exercise 159.2Symmetric Monoidal Categories and Graphical Linear Semantics
  1618. Exercise 159.3Symmetric Monoidal Categories and Graphical Linear Semantics
  1619. Exercise 159.4Symmetric Monoidal Categories and Graphical Linear Semantics
  1620. Exercise 159.5Symmetric Monoidal Categories and Graphical Linear Semantics
  1621. Exercise 159.6Symmetric Monoidal Categories and Graphical Linear Semantics
  1622. Exercise 159.7Symmetric Monoidal Categories and Graphical Linear Semantics
  1623. Exercise 159.8Symmetric Monoidal Categories and Graphical Linear Semantics
  1624. Exercise 159.9 — Practical: a typed diagram normalizerSymmetric Monoidal Categories and Graphical Linear Semantics
  1625. Exercise 160.1Modal and Multimodal Dependent Type Theory
  1626. Exercise 160.2Modal and Multimodal Dependent Type Theory
  1627. Exercise 160.3Modal and Multimodal Dependent Type Theory
  1628. Exercise 160.4Modal and Multimodal Dependent Type Theory
  1629. Exercise 160.5Modal and Multimodal Dependent Type Theory
  1630. Exercise 160.6Modal and Multimodal Dependent Type Theory
  1631. Exercise 160.7Modal and Multimodal Dependent Type Theory
  1632. Exercise 160.8Modal and Multimodal Dependent Type Theory
  1633. Exercise 160.9 — Practical: a multimodal type checkerModal and Multimodal Dependent Type Theory
  1634. Exercise 161.1Synthetic Phase Distinctions and Synthetic Tait Computability
  1635. Exercise 161.2Synthetic Phase Distinctions and Synthetic Tait Computability
  1636. Exercise 161.3Synthetic Phase Distinctions and Synthetic Tait Computability
  1637. Exercise 161.4Synthetic Phase Distinctions and Synthetic Tait Computability
  1638. Exercise 161.5Synthetic Phase Distinctions and Synthetic Tait Computability
  1639. Exercise 161.6Synthetic Phase Distinctions and Synthetic Tait Computability
  1640. Exercise 161.7Synthetic Phase Distinctions and Synthetic Tait Computability
  1641. Exercise 161.8Synthetic Phase Distinctions and Synthetic Tait Computability
  1642. Exercise 161.9Synthetic Phase Distinctions and Synthetic Tait Computability
  1643. Exercise 161.10Synthetic Phase Distinctions and Synthetic Tait Computability
  1644. Exercise 161.11Synthetic Phase Distinctions and Synthetic Tait Computability
  1645. Exercise 162.1Guarded and Clocked Dependent Type Theory
  1646. Exercise 162.2Guarded and Clocked Dependent Type Theory
  1647. Exercise 162.3Guarded and Clocked Dependent Type Theory
  1648. Exercise 162.4Guarded and Clocked Dependent Type Theory
  1649. Exercise 162.5Guarded and Clocked Dependent Type Theory
  1650. Exercise 162.6Guarded and Clocked Dependent Type Theory
  1651. Exercise 162.7Guarded and Clocked Dependent Type Theory
  1652. Exercise 162.8Guarded and Clocked Dependent Type Theory
  1653. Exercise 162.9Guarded and Clocked Dependent Type Theory
  1654. Exercise 163.1Synthetic Guarded Domain Theory and Step-Indexed Semantics
  1655. Exercise 163.2Synthetic Guarded Domain Theory and Step-Indexed Semantics
  1656. Exercise 163.3Synthetic Guarded Domain Theory and Step-Indexed Semantics
  1657. Exercise 163.4Synthetic Guarded Domain Theory and Step-Indexed Semantics
  1658. Exercise 163.5Synthetic Guarded Domain Theory and Step-Indexed Semantics
  1659. Exercise 163.6Synthetic Guarded Domain Theory and Step-Indexed Semantics
  1660. Exercise 163.7Synthetic Guarded Domain Theory and Step-Indexed Semantics
  1661. Exercise 163.8Synthetic Guarded Domain Theory and Step-Indexed Semantics
  1662. Exercise 164.1Dependent Parametricity
  1663. Exercise 164.2Dependent Parametricity
  1664. Exercise 164.3Dependent Parametricity
  1665. Exercise 164.4Dependent Parametricity
  1666. Exercise 164.5Dependent Parametricity
  1667. Exercise 164.6Dependent Parametricity
  1668. Exercise 164.7Dependent Parametricity
  1669. Exercise 164.8Dependent Parametricity
  1670. Exercise 165.1Sized Copattern Recursion and Mixed Induction–Coinduction
  1671. Exercise 165.2Sized Copattern Recursion and Mixed Induction–Coinduction
  1672. Exercise 165.3Sized Copattern Recursion and Mixed Induction–Coinduction
  1673. Exercise 165.4Sized Copattern Recursion and Mixed Induction–Coinduction
  1674. Exercise 165.5Sized Copattern Recursion and Mixed Induction–Coinduction
  1675. Exercise 165.6Sized Copattern Recursion and Mixed Induction–Coinduction
  1676. Exercise 165.7Sized Copattern Recursion and Mixed Induction–Coinduction
  1677. Exercise 166.1Parametric Large Sizes and Realizability Consistency
  1678. Exercise 166.2Parametric Large Sizes and Realizability Consistency
  1679. Exercise 166.3Parametric Large Sizes and Realizability Consistency
  1680. Exercise 166.4Parametric Large Sizes and Realizability Consistency
  1681. Exercise 166.5Parametric Large Sizes and Realizability Consistency
  1682. Exercise 166.6Parametric Large Sizes and Realizability Consistency
  1683. Exercise 167.1Internal Parametricity without an Interval
  1684. Exercise 167.2Internal Parametricity without an Interval
  1685. Exercise 167.3Internal Parametricity without an Interval
  1686. Exercise 167.4Internal Parametricity without an Interval
  1687. Exercise 167.5Internal Parametricity without an Interval
  1688. Exercise 167.6Internal Parametricity without an Interval
  1689. Exercise 167.7Internal Parametricity without an Interval
  1690. Exercise 168.1Reversible Classical Computation
  1691. Exercise 168.2Reversible Classical Computation
  1692. Exercise 168.3Reversible Classical Computation
  1693. Exercise 168.4Reversible Classical Computation
  1694. Exercise 168.5Reversible Classical Computation
  1695. Exercise 169.1Profunctors, Coends, and Optics
  1696. Exercise 169.2Profunctors, Coends, and Optics
  1697. Exercise 169.3Profunctors, Coends, and Optics
  1698. Exercise 169.4Profunctors, Coends, and Optics
  1699. Exercise 169.5Profunctors, Coends, and Optics
  1700. Exercise 169.6Profunctors, Coends, and Optics
  1701. Exercise 170.1Dependent Optics and Indexed Bidirectional Structure
  1702. Exercise 170.2Dependent Optics and Indexed Bidirectional Structure
  1703. Exercise 170.3Dependent Optics and Indexed Bidirectional Structure
  1704. Exercise 170.4Dependent Optics and Indexed Bidirectional Structure
  1705. Exercise 170.5Dependent Optics and Indexed Bidirectional Structure
  1706. Exercise 170.6Dependent Optics and Indexed Bidirectional Structure
  1707. Exercise 171.1Probabilistic Lambda Calculi and Program Equivalence
  1708. Exercise 171.2Probabilistic Lambda Calculi and Program Equivalence
  1709. Exercise 171.3Probabilistic Lambda Calculi and Program Equivalence
  1710. Exercise 171.4Probabilistic Lambda Calculi and Program Equivalence
  1711. Exercise 171.5Probabilistic Lambda Calculi and Program Equivalence
  1712. Exercise 171.6Probabilistic Lambda Calculi and Program Equivalence
  1713. Exercise 171.7Probabilistic Lambda Calculi and Program Equivalence
  1714. Exercise 171.8Probabilistic Lambda Calculi and Program Equivalence
  1715. Exercise 171.9Probabilistic Lambda Calculi and Program Equivalence
  1716. Exercise 171.10Probabilistic Lambda Calculi and Program Equivalence
  1717. Exercise 171.11Probabilistic Lambda Calculi and Program Equivalence
  1718. Exercise 171.12Probabilistic Lambda Calculi and Program Equivalence
  1719. Exercise 171.13Probabilistic Lambda Calculi and Program Equivalence
  1720. Exercise 171.14Probabilistic Lambda Calculi and Program Equivalence
  1721. Exercise 171.15Probabilistic Lambda Calculi and Program Equivalence
  1722. Exercise 171.16Probabilistic Lambda Calculi and Program Equivalence
  1723. Exercise 171.17Probabilistic Lambda Calculi and Program Equivalence
  1724. Exercise 171.18Probabilistic Lambda Calculi and Program Equivalence
  1725. Exercise 171.19Probabilistic Lambda Calculi and Program Equivalence
  1726. Exercise 171.20Probabilistic Lambda Calculi and Program Equivalence
  1727. Exercise 171.21Probabilistic Lambda Calculi and Program Equivalence
  1728. Exercise 171.22Probabilistic Lambda Calculi and Program Equivalence
  1729. Exercise 171.23Probabilistic Lambda Calculi and Program Equivalence
  1730. Exercise 171.24Probabilistic Lambda Calculi and Program Equivalence
  1731. Exercise 171.25Probabilistic Lambda Calculi and Program Equivalence
  1732. Exercise 172.1Probability, Measure, Kernels, and Computable Sampling
  1733. Exercise 172.2Probability, Measure, Kernels, and Computable Sampling
  1734. Exercise 172.3Probability, Measure, Kernels, and Computable Sampling
  1735. Exercise 172.4Probability, Measure, Kernels, and Computable Sampling
  1736. Exercise 172.5Probability, Measure, Kernels, and Computable Sampling
  1737. Exercise 172.6Probability, Measure, Kernels, and Computable Sampling
  1738. Exercise 172.7Probability, Measure, Kernels, and Computable Sampling
  1739. Exercise 172.8Probability, Measure, Kernels, and Computable Sampling
  1740. Exercise 172.9Probability, Measure, Kernels, and Computable Sampling
  1741. Exercise 172.10Probability, Measure, Kernels, and Computable Sampling
  1742. Exercise 172.11Probability, Measure, Kernels, and Computable Sampling
  1743. Exercise 172.12Probability, Measure, Kernels, and Computable Sampling
  1744. Exercise 172.13Probability, Measure, Kernels, and Computable Sampling
  1745. Exercise 172.14Probability, Measure, Kernels, and Computable Sampling
  1746. Exercise 172.15Probability, Measure, Kernels, and Computable Sampling
  1747. Exercise 172.16Probability, Measure, Kernels, and Computable Sampling
  1748. Exercise 173.1Computable Conditioning and Its Limits
  1749. Exercise 173.2Computable Conditioning and Its Limits
  1750. Exercise 173.3Computable Conditioning and Its Limits
  1751. Exercise 173.4Computable Conditioning and Its Limits
  1752. Exercise 173.5Computable Conditioning and Its Limits
  1753. Exercise 173.6Computable Conditioning and Its Limits
  1754. Exercise 173.7Computable Conditioning and Its Limits
  1755. Exercise 173.8Computable Conditioning and Its Limits
  1756. Exercise 173.9Computable Conditioning and Its Limits
  1757. Exercise 173.10Computable Conditioning and Its Limits
  1758. Exercise 173.11Computable Conditioning and Its Limits
  1759. Exercise 173.12Computable Conditioning and Its Limits
  1760. Exercise 173.13Computable Conditioning and Its Limits
  1761. Exercise 173.14Computable Conditioning and Its Limits
  1762. Exercise 174.1Continuous Probabilistic Languages and Quasi-Borel Semantics
  1763. Exercise 174.2Continuous Probabilistic Languages and Quasi-Borel Semantics
  1764. Exercise 174.3Continuous Probabilistic Languages and Quasi-Borel Semantics
  1765. Exercise 174.4Continuous Probabilistic Languages and Quasi-Borel Semantics
  1766. Exercise 174.5Continuous Probabilistic Languages and Quasi-Borel Semantics
  1767. Exercise 174.6Continuous Probabilistic Languages and Quasi-Borel Semantics
  1768. Exercise 174.7Continuous Probabilistic Languages and Quasi-Borel Semantics
  1769. Exercise 174.8Continuous Probabilistic Languages and Quasi-Borel Semantics
  1770. Exercise 174.9Continuous Probabilistic Languages and Quasi-Borel Semantics
  1771. Exercise 174.10Continuous Probabilistic Languages and Quasi-Borel Semantics
  1772. Exercise 174.11Continuous Probabilistic Languages and Quasi-Borel Semantics
  1773. Exercise 175.1Inference as Semantics-Preserving Program Transformation
  1774. Exercise 175.2Inference as Semantics-Preserving Program Transformation
  1775. Exercise 175.3Inference as Semantics-Preserving Program Transformation
  1776. Exercise 175.4Inference as Semantics-Preserving Program Transformation
  1777. Exercise 175.5Inference as Semantics-Preserving Program Transformation
  1778. Exercise 175.6Inference as Semantics-Preserving Program Transformation
  1779. Exercise 175.7Inference as Semantics-Preserving Program Transformation
  1780. Exercise 175.8Inference as Semantics-Preserving Program Transformation
  1781. Exercise 175.9Inference as Semantics-Preserving Program Transformation
  1782. Exercise 175.10Inference as Semantics-Preserving Program Transformation
  1783. Exercise 175.11Inference as Semantics-Preserving Program Transformation
  1784. Exercise 176.1Probabilistic Program Logics
  1785. Exercise 176.2Probabilistic Program Logics
  1786. Exercise 176.3Probabilistic Program Logics
  1787. Exercise 176.4Probabilistic Program Logics
  1788. Exercise 176.5Probabilistic Program Logics
  1789. Exercise 176.6Probabilistic Program Logics
  1790. Exercise 176.7Probabilistic Program Logics
  1791. Exercise 176.8Probabilistic Program Logics
  1792. Exercise 176.9Probabilistic Program Logics
  1793. Exercise 176.10Probabilistic Program Logics
  1794. Exercise 176.11Probabilistic Program Logics
  1795. Exercise 177.1Expected Cost and Probabilistic Resource Analysis
  1796. Exercise 177.2Expected Cost and Probabilistic Resource Analysis
  1797. Exercise 177.3Expected Cost and Probabilistic Resource Analysis
  1798. Exercise 177.4Expected Cost and Probabilistic Resource Analysis
  1799. Exercise 177.5Expected Cost and Probabilistic Resource Analysis
  1800. Exercise 177.6Expected Cost and Probabilistic Resource Analysis
  1801. Exercise 177.7Expected Cost and Probabilistic Resource Analysis
  1802. Exercise 177.8Expected Cost and Probabilistic Resource Analysis
  1803. Exercise 177.9Expected Cost and Probabilistic Resource Analysis
  1804. Exercise 177.10Expected Cost and Probabilistic Resource Analysis
  1805. Exercise 177.11Expected Cost and Probabilistic Resource Analysis
  1806. Exercise 178.1Error Credits and Approximate Higher-Order Reasoning
  1807. Exercise 178.2Error Credits and Approximate Higher-Order Reasoning
  1808. Exercise 178.3Error Credits and Approximate Higher-Order Reasoning
  1809. Exercise 178.4Error Credits and Approximate Higher-Order Reasoning
  1810. Exercise 178.5Error Credits and Approximate Higher-Order Reasoning
  1811. Exercise 178.6Error Credits and Approximate Higher-Order Reasoning
  1812. Exercise 178.7Error Credits and Approximate Higher-Order Reasoning
  1813. Exercise 178.8Error Credits and Approximate Higher-Order Reasoning
  1814. Exercise 178.9Error Credits and Approximate Higher-Order Reasoning
  1815. Exercise 178.10Error Credits and Approximate Higher-Order Reasoning
  1816. Exercise 178.11Error Credits and Approximate Higher-Order Reasoning
  1817. Exercise 179.1Verified Compilation of Probabilistic Programs
  1818. Exercise 179.2Verified Compilation of Probabilistic Programs
  1819. Exercise 179.3Verified Compilation of Probabilistic Programs
  1820. Exercise 179.4Verified Compilation of Probabilistic Programs
  1821. Exercise 179.5Verified Compilation of Probabilistic Programs
  1822. Exercise 179.6Verified Compilation of Probabilistic Programs
  1823. Exercise 179.7Verified Compilation of Probabilistic Programs
  1824. Exercise 179.8Verified Compilation of Probabilistic Programs
  1825. Exercise 180.1Dependent Probability and Fibred Measure
  1826. Exercise 180.2Dependent Probability and Fibred Measure
  1827. Exercise 180.3Dependent Probability and Fibred Measure
  1828. Exercise 180.4Dependent Probability and Fibred Measure
  1829. Exercise 180.5Dependent Probability and Fibred Measure
  1830. Exercise 180.6Dependent Probability and Fibred Measure
  1831. Exercise 180.7Dependent Probability and Fibred Measure
  1832. Exercise 180.8Dependent Probability and Fibred Measure
  1833. Exercise 181.1Differential Lambda Calculus and Resource Taylor Expansion
  1834. Exercise 181.2Differential Lambda Calculus and Resource Taylor Expansion
  1835. Exercise 181.3Differential Lambda Calculus and Resource Taylor Expansion
  1836. Exercise 181.4Differential Lambda Calculus and Resource Taylor Expansion
  1837. Exercise 181.5Differential Lambda Calculus and Resource Taylor Expansion
  1838. Exercise 181.6Differential Lambda Calculus and Resource Taylor Expansion
  1839. Exercise 181.7Differential Lambda Calculus and Resource Taylor Expansion
  1840. Exercise 181.8Differential Lambda Calculus and Resource Taylor Expansion
  1841. Exercise 182.1Differentiable Semantics and Forward-Mode Automatic Differentiation
  1842. Exercise 182.2Differentiable Semantics and Forward-Mode Automatic Differentiation
  1843. Exercise 182.3Differentiable Semantics and Forward-Mode Automatic Differentiation
  1844. Exercise 182.4Differentiable Semantics and Forward-Mode Automatic Differentiation
  1845. Exercise 182.5Differentiable Semantics and Forward-Mode Automatic Differentiation
  1846. Exercise 182.6Differentiable Semantics and Forward-Mode Automatic Differentiation
  1847. Exercise 182.7Differentiable Semantics and Forward-Mode Automatic Differentiation
  1848. Exercise 182.8Differentiable Semantics and Forward-Mode Automatic Differentiation
  1849. Exercise 183.1Reverse-Mode Automatic Differentiation and Cotangent Semantics
  1850. Exercise 183.2Reverse-Mode Automatic Differentiation and Cotangent Semantics
  1851. Exercise 183.3Reverse-Mode Automatic Differentiation and Cotangent Semantics
  1852. Exercise 183.4Reverse-Mode Automatic Differentiation and Cotangent Semantics
  1853. Exercise 183.5Reverse-Mode Automatic Differentiation and Cotangent Semantics
  1854. Exercise 183.6Reverse-Mode Automatic Differentiation and Cotangent Semantics
  1855. Exercise 184.1Quantum Lambda Calculi and Linear Quantum Data
  1856. Exercise 184.2Quantum Lambda Calculi and Linear Quantum Data
  1857. Exercise 184.3Quantum Lambda Calculi and Linear Quantum Data
  1858. Exercise 184.4Quantum Lambda Calculi and Linear Quantum Data
  1859. Exercise 184.5Quantum Lambda Calculi and Linear Quantum Data
  1860. Exercise 184.6Quantum Lambda Calculi and Linear Quantum Data
  1861. Exercise 184.7Quantum Lambda Calculi and Linear Quantum Data
  1862. Exercise 184.8Quantum Lambda Calculi and Linear Quantum Data
  1863. Exercise 184.9Quantum Lambda Calculi and Linear Quantum Data
  1864. Exercise 184.10Quantum Lambda Calculi and Linear Quantum Data
  1865. Exercise 184.11Quantum Lambda Calculi and Linear Quantum Data
  1866. Exercise 184.12Quantum Lambda Calculi and Linear Quantum Data
  1867. Exercise 184.13Quantum Lambda Calculi and Linear Quantum Data
  1868. Exercise 184.14Quantum Lambda Calculi and Linear Quantum Data
  1869. Exercise 184.15Quantum Lambda Calculi and Linear Quantum Data
  1870. Exercise 185.1Typed Quantum Circuits and Proto-Quipper-M
  1871. Exercise 185.2Typed Quantum Circuits and Proto-Quipper-M
  1872. Exercise 185.3Typed Quantum Circuits and Proto-Quipper-M
  1873. Exercise 185.4Typed Quantum Circuits and Proto-Quipper-M
  1874. Exercise 185.5Typed Quantum Circuits and Proto-Quipper-M
  1875. Exercise 185.6Typed Quantum Circuits and Proto-Quipper-M
  1876. Exercise 186.1Linear-Dependent Quantum Programming and Proto-Quipper-D
  1877. Exercise 186.2Linear-Dependent Quantum Programming and Proto-Quipper-D
  1878. Exercise 186.3Linear-Dependent Quantum Programming and Proto-Quipper-D
  1879. Exercise 186.4Linear-Dependent Quantum Programming and Proto-Quipper-D
  1880. Exercise 186.5Linear-Dependent Quantum Programming and Proto-Quipper-D
  1881. Exercise 186.6Linear-Dependent Quantum Programming and Proto-Quipper-D
  1882. Exercise 186.7Linear-Dependent Quantum Programming and Proto-Quipper-D
  1883. Exercise 187.1Elementary Topology and Classical Homotopy
  1884. Exercise 187.2Elementary Topology and Classical Homotopy
  1885. Exercise 187.3Elementary Topology and Classical Homotopy
  1886. Exercise 187.4Elementary Topology and Classical Homotopy
  1887. Exercise 187.5Elementary Topology and Classical Homotopy
  1888. Exercise 187.6Elementary Topology and Classical Homotopy
  1889. Exercise 187.7Elementary Topology and Classical Homotopy
  1890. Exercise 187.8Elementary Topology and Classical Homotopy
  1891. Exercise 187.9Elementary Topology and Classical Homotopy
  1892. Exercise 187.10Elementary Topology and Classical Homotopy
  1893. Exercise 187.11Elementary Topology and Classical Homotopy
  1894. Exercise 187.12Elementary Topology and Classical Homotopy
  1895. Exercise 187.13Elementary Topology and Classical Homotopy
  1896. Exercise 187.14Elementary Topology and Classical Homotopy
  1897. Exercise 187.15Elementary Topology and Classical Homotopy
  1898. Exercise 187.16Elementary Topology and Classical Homotopy
  1899. Exercise 187.17Elementary Topology and Classical Homotopy
  1900. Exercise 187.18Elementary Topology and Classical Homotopy
  1901. Exercise 187.19Elementary Topology and Classical Homotopy
  1902. Exercise 188.1Fibrations, Homotopy Groups, and Exact Sequences
  1903. Exercise 188.2Fibrations, Homotopy Groups, and Exact Sequences
  1904. Exercise 188.3Fibrations, Homotopy Groups, and Exact Sequences
  1905. Exercise 188.4Fibrations, Homotopy Groups, and Exact Sequences
  1906. Exercise 188.5Fibrations, Homotopy Groups, and Exact Sequences
  1907. Exercise 188.6Fibrations, Homotopy Groups, and Exact Sequences
  1908. Exercise 188.7Fibrations, Homotopy Groups, and Exact Sequences
  1909. Exercise 188.8Fibrations, Homotopy Groups, and Exact Sequences
  1910. Exercise 188.9Fibrations, Homotopy Groups, and Exact Sequences
  1911. Exercise 188.10Fibrations, Homotopy Groups, and Exact Sequences
  1912. Exercise 188.11Fibrations, Homotopy Groups, and Exact Sequences
  1913. Exercise 62.1Types as ∞-Groupoids
  1914. Exercise 62.2Types as ∞-Groupoids
  1915. Exercise 62.3Types as ∞-Groupoids
  1916. Exercise 62.4Types as ∞-Groupoids
  1917. Exercise 62.5Types as ∞-Groupoids
  1918. Exercise 62.6Types as ∞-Groupoids
  1919. Exercise 62.7Types as ∞-Groupoids
  1920. Exercise 62.8Types as ∞-Groupoids
  1921. Exercise 62.9Types as ∞-Groupoids
  1922. Exercise 62.10Types as ∞-Groupoids
  1923. Exercise 62.11Types as ∞-Groupoids
  1924. Exercise 62.12Types as ∞-Groupoids
  1925. Exercise 62.13Types as ∞-Groupoids
  1926. Exercise 62.14Types as ∞-Groupoids
  1927. Exercise 62.15Types as ∞-Groupoids
  1928. Exercise 189.16Types as ∞-Groupoids
  1929. Exercise 189.17Types as ∞-Groupoids
  1930. Exercise 190.1Simplicial Sets, Horns, and Kan Fibrations
  1931. Exercise 190.2Simplicial Sets, Horns, and Kan Fibrations
  1932. Exercise 190.3Simplicial Sets, Horns, and Kan Fibrations
  1933. Exercise 190.4Simplicial Sets, Horns, and Kan Fibrations
  1934. Exercise 190.5Simplicial Sets, Horns, and Kan Fibrations
  1935. Exercise 190.6Simplicial Sets, Horns, and Kan Fibrations
  1936. Exercise 190.7Simplicial Sets, Horns, and Kan Fibrations
  1937. Exercise 190.8Simplicial Sets, Horns, and Kan Fibrations
  1938. Exercise 65.1Univalence
  1939. Exercise 65.2Univalence
  1940. Exercise 65.4Univalence
  1941. Exercise 65.3Univalence
  1942. Exercise 65.5Univalence
  1943. Exercise 65.6Univalence
  1944. Exercise 65.7Univalence
  1945. Exercise 65.8Univalence
  1946. Exercise 65.9Univalence
  1947. Exercise 65.10Univalence
  1948. Exercise 65.11Univalence
  1949. Exercise 65.12Univalence
  1950. Exercise 65.13Univalence
  1951. Exercise 65.14Univalence
  1952. Exercise 65.15Univalence
  1953. Exercise 193.16Univalence
  1954. Exercise 193.17Univalence
  1955. Exercise 66.1Truncation Levels, Propositions, and Logic
  1956. Exercise 66.2Truncation Levels, Propositions, and Logic
  1957. Exercise 66.3Truncation Levels, Propositions, and Logic
  1958. Exercise 66.4Truncation Levels, Propositions, and Logic
  1959. Exercise 66.5Truncation Levels, Propositions, and Logic
  1960. Exercise 66.6Truncation Levels, Propositions, and Logic
  1961. Exercise 66.7Truncation Levels, Propositions, and Logic
  1962. Exercise 66.8Truncation Levels, Propositions, and Logic
  1963. Exercise 66.9Truncation Levels, Propositions, and Logic
  1964. Exercise 66.10Truncation Levels, Propositions, and Logic
  1965. Exercise 66.11Truncation Levels, Propositions, and Logic
  1966. Exercise 66.13Truncation Levels, Propositions, and Logic
  1967. Exercise 66.14Truncation Levels, Propositions, and Logic
  1968. Exercise 66.15Truncation Levels, Propositions, and Logic
  1969. Exercise 66.12Truncation Levels, Propositions, and Logic
  1970. Exercise 66.16Truncation Levels, Propositions, and Logic
  1971. Exercise 66.17Truncation Levels, Propositions, and Logic
  1972. Exercise 66.18Truncation Levels, Propositions, and Logic
  1973. Exercise 66.19Truncation Levels, Propositions, and Logic
  1974. Exercise 66.20Truncation Levels, Propositions, and Logic
  1975. Exercise 66.21Truncation Levels, Propositions, and Logic
  1976. Exercise 66.22Truncation Levels, Propositions, and Logic
  1977. Exercise 66.23Truncation Levels, Propositions, and Logic
  1978. Exercise 66.24Truncation Levels, Propositions, and Logic
  1979. Exercise 66.25Truncation Levels, Propositions, and Logic
  1980. Exercise 66.26Truncation Levels, Propositions, and Logic
  1981. Exercise 195.27Truncation Levels, Propositions, and Logic
  1982. Exercise 195.28Truncation Levels, Propositions, and Logic
  1983. Exercise 68.1Higher Inductive Types and Homotopy-Initiality
  1984. Exercise 68.2Higher Inductive Types and Homotopy-Initiality
  1985. Exercise 68.3Higher Inductive Types and Homotopy-Initiality
  1986. Exercise 68.4Higher Inductive Types and Homotopy-Initiality
  1987. Exercise 68.5Higher Inductive Types and Homotopy-Initiality
  1988. Exercise 68.6Higher Inductive Types and Homotopy-Initiality
  1989. Exercise 68.7Higher Inductive Types and Homotopy-Initiality
  1990. Exercise 68.8Higher Inductive Types and Homotopy-Initiality
  1991. Exercise 68.9Higher Inductive Types and Homotopy-Initiality
  1992. Exercise 68.10Higher Inductive Types and Homotopy-Initiality
  1993. Exercise 68.11Higher Inductive Types and Homotopy-Initiality
  1994. Exercise 68.12Higher Inductive Types and Homotopy-Initiality
  1995. Exercise 68.13Higher Inductive Types and Homotopy-Initiality
  1996. Exercise 68.14Higher Inductive Types and Homotopy-Initiality
  1997. Exercise 68.15Higher Inductive Types and Homotopy-Initiality
  1998. Exercise 68.16Higher Inductive Types and Homotopy-Initiality
  1999. Exercise 68.17Higher Inductive Types and Homotopy-Initiality
  2000. Exercise 68.18Higher Inductive Types and Homotopy-Initiality
  2001. Exercise 68.19Higher Inductive Types and Homotopy-Initiality
  2002. Exercise 68.20Higher Inductive Types and Homotopy-Initiality
  2003. Exercise 68.21Higher Inductive Types and Homotopy-Initiality
  2004. Exercise 68.22Higher Inductive Types and Homotopy-Initiality
  2005. Exercise 68.23Higher Inductive Types and Homotopy-Initiality
  2006. Exercise 68.24Higher Inductive Types and Homotopy-Initiality
  2007. Exercise 198.25Higher Inductive Types and Homotopy-Initiality
  2008. Exercise 198.26Higher Inductive Types and Homotopy-Initiality
  2009. Exercise 69.1Coverings, van Kampen, and the Fundamental Group
  2010. Exercise 69.2Coverings, van Kampen, and the Fundamental Group
  2011. Exercise 69.3Coverings, van Kampen, and the Fundamental Group
  2012. Exercise 69.4Coverings, van Kampen, and the Fundamental Group
  2013. Exercise 69.5Coverings, van Kampen, and the Fundamental Group
  2014. Exercise 69.6Coverings, van Kampen, and the Fundamental Group
  2015. Exercise 69.7Coverings, van Kampen, and the Fundamental Group
  2016. Exercise 202.8Coverings, van Kampen, and the Fundamental Group
  2017. Exercise 202.9Coverings, van Kampen, and the Fundamental Group
  2018. Exercise 202.10Coverings, van Kampen, and the Fundamental Group
  2019. Exercise 202.11Coverings, van Kampen, and the Fundamental Group
  2020. Exercise 202.12Coverings, van Kampen, and the Fundamental Group
  2021. Exercise 202.13Coverings, van Kampen, and the Fundamental Group
  2022. Exercise 74.1Univalent Categories and Rezk Completion
  2023. Exercise 74.2Univalent Categories and Rezk Completion
  2024. Exercise 74.3Univalent Categories and Rezk Completion
  2025. Exercise 74.4Univalent Categories and Rezk Completion
  2026. Exercise 74.5Univalent Categories and Rezk Completion
  2027. Exercise 74.6Univalent Categories and Rezk Completion
  2028. Exercise 74.7Univalent Categories and Rezk Completion
  2029. Exercise 74.8Univalent Categories and Rezk Completion
  2030. Exercise 74.9Univalent Categories and Rezk Completion
  2031. Exercise 74.10Univalent Categories and Rezk Completion
  2032. Exercise 74.11Univalent Categories and Rezk Completion
  2033. Exercise 74.12Univalent Categories and Rezk Completion
  2034. Exercise 74.13Univalent Categories and Rezk Completion
  2035. Exercise 207.14Univalent Categories and Rezk Completion
  2036. Exercise 207.15Univalent Categories and Rezk Completion
  2037. Exercise 74.14Set-Level Mathematics in Univalent Foundations
  2038. Exercise 74.15Set-Level Mathematics in Univalent Foundations
  2039. Exercise 74.16Set-Level Mathematics in Univalent Foundations
  2040. Exercise 210.4Set-Level Mathematics in Univalent Foundations
  2041. Exercise 210.5Set-Level Mathematics in Univalent Foundations
  2042. Exercise 74.17Completions and the Real Numbers
  2043. Exercise 74.18Completions and the Real Numbers
  2044. Exercise 211.3Completions and the Real Numbers
  2045. Exercise 211.4Completions and the Real Numbers
  2046. Exercise 74.19Choice-Free HII Cauchy Completion
  2047. Exercise 74.20Choice-Free HII Cauchy Completion
  2048. Exercise 79.1Observational Equality and Computational Extensionality
  2049. Exercise 79.2Observational Equality and Computational Extensionality
  2050. Exercise 79.3Observational Equality and Computational Extensionality
  2051. Exercise 79.4Observational Equality and Computational Extensionality
  2052. Exercise 79.5Observational Equality and Computational Extensionality
  2053. Exercise 79.6Observational Equality and Computational Extensionality
  2054. Exercise 79.7Observational Equality and Computational Extensionality
  2055. Exercise 79.8Observational Equality and Computational Extensionality
  2056. Exercise 79.9Observational Equality and Computational Extensionality
  2057. Exercise 79.10Observational Equality and Computational Extensionality
  2058. Exercise 79.11Observational Equality and Computational Extensionality
  2059. Exercise 79.12Observational Equality and Computational Extensionality
  2060. Exercise 79.13Observational Equality and Computational Extensionality
  2061. Exercise 79.14Observational Equality and Computational Extensionality
  2062. Exercise 79.15Observational Equality and Computational Extensionality
  2063. Exercise 79.16Observational Equality and Computational Extensionality
  2064. Exercise 215.17Observational Equality and Computational Extensionality
  2065. Exercise 215.18Observational Equality and Computational Extensionality
  2066. Exercise 80.1Cubical Type Theory I: De Morgan Cubes
  2067. Exercise 80.2Cubical Type Theory I: De Morgan Cubes
  2068. Exercise 80.3Cubical Type Theory I: De Morgan Cubes
  2069. Exercise 80.4Cubical Type Theory I: De Morgan Cubes
  2070. Exercise 80.5Cubical Type Theory I: De Morgan Cubes
  2071. Exercise 80.6Cubical Type Theory I: De Morgan Cubes
  2072. Exercise 80.7Cubical Type Theory I: De Morgan Cubes
  2073. Exercise 80.8Cubical Type Theory I: De Morgan Cubes
  2074. Exercise 80.9Cubical Type Theory I: De Morgan Cubes
  2075. Exercise 80.10Cubical Type Theory I: De Morgan Cubes
  2076. Exercise 80.11Cubical Type Theory I: De Morgan Cubes
  2077. Exercise 80.12Cubical Type Theory I: De Morgan Cubes
  2078. Exercise 80.13Cubical Type Theory I: De Morgan Cubes
  2079. Exercise 80.14Cubical Type Theory I: De Morgan Cubes
  2080. Exercise 80.15Cubical Type Theory I: De Morgan Cubes
  2081. Exercise 80.16Cubical Type Theory I: De Morgan Cubes
  2082. Exercise 80.17Cubical Type Theory I: De Morgan Cubes
  2083. Exercise 80.18Cubical Type Theory I: De Morgan Cubes
  2084. Exercise 80.19Cubical Type Theory I: De Morgan Cubes
  2085. Exercise 80.20Cubical Type Theory I: De Morgan Cubes
  2086. Exercise 217.21Cubical Type Theory I: De Morgan Cubes
  2087. Exercise 217.22Cubical Type Theory I: De Morgan Cubes
  2088. Exercise 81.1Cubical Type Theory II: Cartesian Cubes and Computation
  2089. Exercise 81.2Cubical Type Theory II: Cartesian Cubes and Computation
  2090. Exercise 81.3Cubical Type Theory II: Cartesian Cubes and Computation
  2091. Exercise 81.4Cubical Type Theory II: Cartesian Cubes and Computation
  2092. Exercise 81.5Cubical Type Theory II: Cartesian Cubes and Computation
  2093. Exercise 81.6Cubical Type Theory II: Cartesian Cubes and Computation
  2094. Exercise 81.7Cubical Type Theory II: Cartesian Cubes and Computation
  2095. Exercise 81.8Cubical Type Theory II: Cartesian Cubes and Computation
  2096. Exercise 81.9Cubical Type Theory II: Cartesian Cubes and Computation
  2097. Exercise 81.10Cubical Type Theory II: Cartesian Cubes and Computation
  2098. Exercise 81.11Cubical Type Theory II: Cartesian Cubes and Computation
  2099. Exercise 81.12Cubical Type Theory II: Cartesian Cubes and Computation
  2100. Exercise 81.13Cubical Type Theory II: Cartesian Cubes and Computation
  2101. Exercise 81.14Cubical Type Theory II: Cartesian Cubes and Computation
  2102. Exercise 81.15Cubical Type Theory II: Cartesian Cubes and Computation
  2103. Exercise 81.16Cubical Type Theory II: Cartesian Cubes and Computation
  2104. Exercise 218.17Cubical Type Theory II: Cartesian Cubes and Computation
  2105. Exercise 218.18Cubical Type Theory II: Cartesian Cubes and Computation

Search the book

Type to search the local edition.