Lectures onType Theory
Terms
Scholarly index

Terms

  1. judgmentchapter-001
  2. judgment formchapter-001
  3. rulechapter-001
  4. premiseschapter-001
  5. conclusionchapter-001
  6. derivationchapter-001
  7. syntactic objectschapter-001
  8. instancechapter-001
  9. subjectschapter-001
  10. axiomchapter-001
  11. rule setchapter-001
  12. metavariablechapter-001
  13. rule schemechapter-001
  14. side conditionchapter-001
  15. rule-closed setchapter-001
  16. inductive definitionchapter-001
  17. nonterminalchapter-001
  18. productionchapter-001
  19. context-free grammarchapter-001
  20. start symbolchapter-001
  21. terminal symbolschapter-001
  22. parse treeschapter-001
  23. constructor countchapter-001
  24. heightchapter-001
  25. effective codechapter-001
  26. semidecidablechapter-001
  27. decidablechapter-001
  28. rule inductionchapter-001
  29. induction hypotheseschapter-001
  30. iterated inductive definitionchapter-001
  31. simultaneous inductive definitionchapter-001
  32. inversionchapter-001
  33. primitive rulechapter-001
  34. hypothetical derivabilitychapter-001
  35. admissible rulechapter-001
  36. valuechapter-001
  37. congruence ruleschapter-001
  38. Raw termschapter-001
  39. untypedchapter-001
  40. closed termchapter-001
  41. fresh renamingchapter-001
  42. Alpha-equivalencechapter-001
  43. alpha-equivalence classchapter-001
  44. quotient termchapter-001
  45. Capture-avoiding substitutionchapter-001
  46. operational semanticschapter-001
  47. dynamicschapter-001
  48. contractumchapter-001
  49. reflexive-transitive closurechapter-001
  50. evaluation contextchapter-001
  51. redexchapter-001
  52. stuck termchapter-001
  53. big-step judgmentchapter-001
  54. Divergencechapter-001
  55. simple typeschapter-002
  56. raw termschapter-002
  57. termchapter-002
  58. contextchapter-002
  59. declaration-preserving extensionchapter-002
  60. typing judgmentchapter-002
  61. Valueschapter-002
  62. inhabitantchapter-002
  63. introduction ruleschapter-002
  64. elimination ruleschapter-002
  65. scrutineechapter-002
  66. injection-free termschapter-002
  67. propositional letterchapter-002
  68. propositional formulaschapter-002
  69. excluded middlechapter-002
  70. double-negation eliminationchapter-002
  71. logical skeletonchapter-002
  72. proof contextchapter-002
  73. Strong normalizationchapter-002
  74. neutral termchapter-002
  75. reducible termschapter-002
  76. quantifierchapter-003
  77. intermediate formulachapter-003
  78. first-order signaturechapter-003
  79. Termschapter-003
  80. formulaschapter-003
  81. abstract binding treechapter-003
  82. rankchapter-003
  83. object languagechapter-003
  84. metalanguagechapter-003
  85. eigenvariablechapter-003
  86. major premisechapter-003
  87. minor premisechapter-003
  88. interpretationchapter-003
  89. assignmentchapter-003
  90. validchapter-003
  91. sequentchapter-003
  92. principal formulachapter-003
  93. side formulaschapter-003
  94. primitive recursionchapter-003
  95. continuationchapter-003
  96. proof-label substitutionchapter-003
  97. individual substitutionchapter-003
  98. semidecidablechapter-003
  99. search statechapter-003
  100. eigenparameterschapter-003
  101. parametric polymorphismchapter-004
  102. polymorphismchapter-004
  103. type schemechapter-004
  104. type variableschapter-004
  105. signaturechapter-004
  106. type constructorschapter-004
  107. Monotypeschapter-004
  108. substitutionchapter-004
  109. HM contextschapter-004
  110. instancechapter-004
  111. equation problemchapter-004
  112. most general unifierchapter-004
  113. partial functionchapter-004
  114. legal fresh supplychapter-004
  115. residual equation problemchapter-004
  116. kindschapter-004
  117. monomorphic-recursion baselinechapter-005
  118. occurs checkchapter-005
  119. matcheschapter-005
  120. semi-unification problemchapter-005
  121. semi-unifierchapter-005
  122. nongeneric variableschapter-005
  123. syntax-directed Milner–Mycroft judgmentchapter-005
  124. de Bruijn indexchapter-005
  125. prefix-tree orderchapter-005
  126. log-space many-one reductionchapter-005
  127. maximal nonproduct componentchapter-005
  128. one-tape Turing machinechapter-005
  129. computablechapter-005
  130. many-one reduceschapter-005
  131. decideschapter-005
  132. undecidablechapter-005
  133. recursively enumerablechapter-005
  134. r.e.-hardchapter-005
  135. r.e.-completechapter-005
  136. rigid constantschapter-005
  137. flexible variableschapter-005
  138. well scopedchapter-005
  139. rigid escapechapter-005
  140. indexedchapter-006
  141. dimension variableschapter-006
  142. normalized dimension expressionchapter-006
  143. dimension-variable substitutionchapter-006
  144. free abelianchapter-006
  145. unit environmentchapter-006
  146. unitchapter-006
  147. scalechapter-006
  148. closed dimensionchapter-006
  149. principal familychapter-006
  150. unimodularchapter-006
  151. integer latticechapter-006
  152. principal dimension solverchapter-006
  153. solveschapter-006
  154. G_ r-relative solutionchapter-006
  155. ternary relationchapter-006
  156. unary predicatechapter-006
  157. canonical numeric corechapter-006
  158. core valuechapter-006
  159. core normal formchapter-006
  160. core neutralchapter-006
  161. neutral normal formchapter-006
  162. terminal outcomechapter-006
  163. deterministicchapter-006
  164. template environmentchapter-006
  165. specialization semanticschapter-006
  166. scale characterchapter-006
  167. unit-change logical relationchapter-006
  168. χ-related at Γ[κ] over γ,γ'chapter-006
  169. scale erasure of a core termchapter-006
  170. scale companionschapter-006
  171. modulechapter-006
  172. Separate compilationchapter-006
  173. linkingchapter-006
  174. recordchapter-007
  175. labelschapter-007
  176. fieldchapter-007
  177. variantchapter-007
  178. indexed coproductchapter-007
  179. rowchapter-007
  180. lacks predicatechapter-007
  181. predicate contextchapter-007
  182. admissible substitutionchapter-007
  183. Row equalitychapter-007
  184. target-admissiblechapter-007
  185. Church-stylechapter-008
  186. kind assignmentchapter-008
  187. record kindchapter-008
  188. respectschapter-008
  189. weakeningchapter-008
  190. index typechapter-008
  191. index assignmentchapter-008
  192. ground substitutionchapter-008
  193. numeral substitutionchapter-008
  194. second-orderchapter-009
  195. metatheorychapter-009
  196. Turing machinechapter-009
  197. annotated termchapter-009
  198. impredicative quantifierchapter-009
  199. exchange rulechapter-009
  200. reducibility candidatechapter-009
  201. Strong normalizationchapter-009
  202. neutral termchapter-009
  203. full-function interpretation packagechapter-009
  204. T-algebrachapter-009
  205. T-algebra homomorphismchapter-009
  206. weakly initialchapter-009
  207. initialchapter-009
  208. idempotentchapter-009
  209. splittingchapter-009
  210. stablechapter-009
  211. cardinalchapter-009
  212. de Bruijn indiceschapter-009
  213. logical relationchapter-010
  214. graph relationchapter-010
  215. relation environmentchapter-010
  216. identity extension at Achapter-010
  217. pointed ω-cpochapter-010
  218. continuouschapter-010
  219. strictchapter-010
  220. admissiblechapter-010
  221. kindschapter-011
  222. constructorschapter-011
  223. kind contextchapter-011
  224. Type-level reductionchapter-011
  225. normal constructorchapter-011
  226. neutral constructorchapter-011
  227. implementationchapter-012
  228. abstract interfacechapter-012
  229. clientchapter-012
  230. Opaque sealingchapter-012
  231. existential packagechapter-012
  232. Representation independencechapter-012
  233. classchapter-013
  234. methodschapter-013
  235. instancechapter-013
  236. dictionarychapter-013
  237. superclasschapter-013
  238. coherencechapter-013
  239. evidence telescopechapter-013
  240. evidence storechapter-013
  241. resolution selectorchapter-013
  242. Resolutionchapter-013
  243. Canonical predicate normalizationchapter-013
  244. signaturechapter-014
  245. modulechapter-014
  246. projectible pathchapter-014
  247. manifest atomchapter-014
  248. open module-value judgmentchapter-014
  249. operational module valueschapter-014
  250. hereditary module substitutionchapter-014
  251. projectible viewchapter-014
  252. proof-relevant relationchapter-014
  253. polar componentchapter-015
  254. atomic class signaturechapter-016
  255. adoptionchapter-016
  256. resolverchapter-016
  257. quotationchapter-017
  258. shallow prequotationchapter-017
  259. deep prequotationchapter-017
  260. neutral termschapter-017
  261. subtypechapter-018
  262. width subtypingchapter-018
  263. depth subtypingchapter-018
  264. permutation invariancechapter-018
  265. recursive boundschapter-018
  266. polar typechapter-019
  267. polar schemechapter-019
  268. bisubstitutionchapter-019
  269. stablechapter-019
  270. local polar type automatonchapter-019
  271. intersection typechapter-020
  272. union typechapter-020
  273. atomchapter-020
  274. well-shaped interfacechapter-020
  275. universal finite-graph domainchapter-020
  276. Semantic subtypingchapter-020
  277. ordinary typechapter-021
  278. disjointchapter-021
  279. ordinary leafchapter-021
  280. refinement typechapter-022
  281. difference-logic fragmentchapter-022
  282. bind compositionchapter-022
  283. path certificatechapter-022
  284. contradiction certificatechapter-022
  285. verification conditionchapter-022
  286. unknown typechapter-023
  287. castchapter-023
  288. gradual typeschapter-023
  289. consistency relationchapter-023
  290. Ground typeschapter-023
  291. Precisionchapter-023
  292. recursive typechapter-024
  293. iso-recursive calculuschapter-024
  294. contractive recursive typechapter-024
  295. bisimulationchapter-024
  296. posetchapter-024
  297. omega-chainchapter-024
  298. omega-cpochapter-024
  299. pointed omega-cpochapter-024
  300. domainchapter-024
  301. monotone functionchapter-024
  302. continuous functionchapter-024
  303. receiver binderchapter-025
  304. objectchapter-025
  305. Weak object reductionchapter-025
  306. Width-invariant object subtypingchapter-025
  307. complete set of unifierschapter-026
  308. Self typechapter-027
  309. F-boundchapter-027
  310. protocolchapter-027
  311. Matchingchapter-027
  312. well-founded operation treechapter-028
  313. bindchapter-028
  314. monadchapter-028
  315. effect theorychapter-028
  316. Kleisli substitutionchapter-028
  317. foldchapter-028
  318. pinchapter-028
  319. administrative closurechapter-028
  320. scoped signaturechapter-029
  321. explicit substitutionchapter-029
  322. reindexingchapter-029
  323. higher-order effect signaturechapter-030
  324. hefty treeschapter-030
  325. forkchapter-030
  326. hefty bindchapter-030
  327. hefty algebrachapter-030
  328. hefty catamorphismchapter-030
  329. elaborationchapter-030
  330. handlerchapter-031
  331. Effect rowschapter-031
  332. row equivalencechapter-031
  333. internal-safechapter-031
  334. effect capabilitychapter-032
  335. lexical tunnellingchapter-032
  336. generated configurationchapter-032
  337. undelimited capabilitychapter-032
  338. ownership capabilitychapter-032
  339. capture setchapter-032
  340. locality/effect reflectionchapter-032
  341. control-flow linearitychapter-032
  342. effect structurechapter-033
  343. complex valueschapter-033
  344. exchangerchapter-034
  345. trampolinechapter-034
  346. cluechapter-034
  347. hopperchapter-034
  348. mainline callchapter-034
  349. continuationchapter-035
  350. control operatorchapter-035
  351. framechapter-035
  352. stackchapter-035
  353. continuation-passing stylechapter-035
  354. linear contextchapter-036
  355. multiplicative connectiveschapter-036
  356. additive connectiveschapter-036
  357. commuting conversionchapter-036
  358. compatible closurechapter-037
  359. exponential assumptionchapter-037
  360. ordered contextchapter-038
  361. sequentchapter-038
  362. ordered cutchapter-038
  363. invertible rulechapter-039
  364. inversion phasechapter-039
  365. focusing phasechapter-039
  366. polaritychapter-039
  367. stable succedentchapter-039
  368. suspension-normal persistent contextchapter-039
  369. proof structurechapter-040
  370. correction graphchapter-040
  371. switchingchapter-040
  372. Danos–Regnier correctness criterionchapter-040
  373. proof netchapter-040
  374. regularchapter-040
  375. maximalchapter-040
  376. interaction netchapter-041
  377. active pairchapter-041
  378. principal portchapter-041
  379. auxiliary portschapter-041
  380. netchapter-041
  381. interfacechapter-041
  382. interaction systemchapter-041
  383. normal formchapter-041
  384. INAMBchapter-041
  385. angelic mergechapter-041
  386. infinity mergechapter-041
  387. INMPPchapter-041
  388. INMPP-normalchapter-041
  389. Graft rulechapter-041
  390. shallow formchapter-041
  391. permanently livechapter-041
  392. L'evy familychapter-042
  393. buschapter-042
  394. main levelchapter-042
  395. rightmost wireschapter-042
  396. graph normal formchapter-042
  397. reachable and well formed for Pchapter-042
  398. access pathchapter-042
  399. redex labelchapter-042
  400. parallel beta stepchapter-042
  401. first-class machine modelchapter-042
  402. bunchchapter-043
  403. one-hole bunch contextchapter-043
  404. structural congruencechapter-043
  405. closedchapter-043
  406. resource framechapter-043
  407. resource modelchapter-043
  408. forcing relationchapter-043
  409. subheapchapter-044
  410. separating conjunctionchapter-044
  411. heap assertionchapter-044
  412. separating implicationchapter-044
  413. Localitychapter-044
  414. local commandchapter-044
  415. semantic Hoare triplechapter-044
  416. affinechapter-045
  417. persistentchapter-045
  418. fancy updatechapter-045
  419. abortchapter-045
  420. commitchapter-045
  421. ownerchapter-046
  422. shared borrowchapter-046
  423. exclusive borrowchapter-046
  424. safechapter-046
  425. Swiftlet expressionchapter-049
  426. independentchapter-049
  427. well formedchapter-049
  428. well typedchapter-049
  429. region effectchapter-050
  430. type with placechapter-050
  431. arrow effectchapter-050
  432. connectschapter-050
  433. region handlechapter-050
  434. capability variablechapter-050
  435. duplicable authoritychapter-050
  436. unique authoritychapter-050
  437. stripping operationchapter-050
  438. memorychapter-050
  439. memory typechapter-050
  440. region typechapter-050
  441. live-region effectchapter-050
  442. capture setchapter-051
  443. protocol transitionchapter-052
  444. coeffect scalar structurechapter-053
  445. flat coeffectchapter-053
  446. pure valuechapter-053
  447. top-pointedchapter-053
  448. bottom-pointedchapter-053
  449. structural coeffectchapter-053
  450. locally soundchapter-053
  451. locally completechapter-053
  452. realizeschapter-053
  453. preordered semiringchapter-054
  454. Linear Basechapter-054
  455. Graded Basechapter-054
  456. later typechapter-055
  457. stable modalitychapter-055
  458. token-freechapter-055
  459. tick-freechapter-055
  460. stablechapter-055
  461. worldchapter-055
  462. Soft Linear Logicchapter-056
  463. degreechapter-056
  464. rankchapter-056
  465. weightchapter-056
  466. potentialchapter-057
  467. heap-cell metricchapter-057
  468. list annotationchapter-057
  469. sharing relationchapter-057
  470. livechapter-058
  471. contractivechapter-058
  472. tail-recursionchapter-058
  473. projectablechapter-059
  474. linearchapter-059
  475. coherentchapter-059
  476. block setchapter-059
  477. mergechapter-059
  478. sortschapter-060
  479. pure-type-system specificationchapter-060
  480. PTS specificationchapter-060
  481. axiomschapter-060
  482. product tripleschapter-060
  483. pseudo-termschapter-060
  484. Compatible beta-reductionchapter-060
  485. neutralchapter-060
  486. Calculus of Constructionschapter-060
  487. legalchapter-060
  488. legal in Γchapter-060
  489. functionalchapter-060
  490. lookup-effectivechapter-060
  491. Edinburgh Logical Frameworkchapter-061
  492. LFchapter-061
  493. atomic LF objectchapter-061
  494. canonical LF objectchapter-061
  495. judgments-as-types representationchapter-061
  496. higher-order abstract syntaxchapter-061
  497. HOASchapter-061
  498. compositionalchapter-061
  499. adequatechapter-061
  500. typed de Bruijn variablechapter-061
  501. de Bruijn renamingchapter-061
  502. de Bruijn substitutionchapter-061
  503. locally nameless termchapter-061
  504. locally closedchapter-061
  505. parametric higher-order abstract syntaxchapter-061
  506. PHOAS termchapter-061
  507. parametricchapter-061
  508. contextual objectchapter-061
  509. atomschapter-062
  510. finite permutationchapter-062
  511. supportschapter-062
  512. nominal setchapter-062
  513. a is fresh for xchapter-062
  514. equivariantchapter-062
  515. name abstractionchapter-062
  516. alpha-equivalencechapter-062
  517. meta-variableschapter-063
  518. contextual typechapter-063
  519. hereditary substitutionchapter-063
  520. underapproximates Ψ with respect to σchapter-063
  521. context schemachapter-063
  522. atomschapter-064
  523. permutation actionchapter-064
  524. supportschapter-064
  525. concretionchapter-064
  526. finite typechapter-067
  527. double-negation shiftchapter-067
  528. selection typechapter-067
  529. relativized bar inductionchapter-067
  530. total continuous functionalschapter-067
  531. state collecting semanticschapter-068
  532. Galois connectionchapter-068
  533. Galois insertionchapter-068
  534. Syntactic-path soundnesschapter-068
  535. Semantic-trace soundnesschapter-068
  536. binding treechapter-071
  537. binding signaturechapter-071
  538. operatorschapter-071
  539. aritychapter-071
  540. raw expressionschapter-071
  541. raw contextchapter-071
  542. telescopechapter-071
  543. fresh renamingchapter-071
  544. alpha-equivalencechapter-071
  545. expressionchapter-071
  546. capture-avoiding substitutionchapter-071
  547. simultaneous substitutionchapter-071
  548. presuppositionschapter-071
  549. judgment theseschapter-071
  550. family of types over Achapter-071
  551. sectionchapter-071
  552. fiberchapter-071
  553. structural ruleschapter-071
  554. economical presentationchapter-071
  555. structural stabilitychapter-071
  556. context substitutionchapter-071
  557. relative telescope mapchapter-071
  558. dependent productchapter-072
  559. formationchapter-072
  560. introductionchapter-072
  561. eliminationchapter-072
  562. computationchapter-072
  563. uniquenesschapter-072
  564. dependent sumchapter-072
  565. unit typechapter-072
  566. definitional isomorphismchapter-072
  567. inductive familychapter-073
  568. empty typechapter-073
  569. recursorchapter-073
  570. booleanschapter-073
  571. coproductchapter-073
  572. natural numberschapter-073
  573. well-founded treeschapter-073
  574. polynomial inductive signaturechapter-073
  575. strict positivitychapter-073
  576. Aczel rule setchapter-073
  577. deterministicchapter-073
  578. universechapter-074
  579. Russell presentationchapter-074
  580. _i-smallchapter-074
  581. level variableschapter-074
  582. large eliminationchapter-074
  583. cumulative membershipchapter-074
  584. explicit strict liftchapter-074
  585. codechapter-075
  586. Tarski universechapter-075
  587. erasurechapter-075
  588. decorationchapter-075
  589. comparison-alignedchapter-075
  590. large universechapter-076
  591. intensional identity typechapter-077
  592. identity familychapter-077
  593. identificationchapter-077
  594. equality reflectionchapter-077
  595. path-induction patternchapter-077
  596. transportchapter-077
  597. singletonchapter-077
  598. centerchapter-077
  599. function extensionalitychapter-077
  600. uniqueness of identity proofschapter-077
  601. axiom Kchapter-077
  602. indexed inductive familychapter-078
  603. pattern clausechapter-078
  604. coveragechapter-078
  605. inaccessible patternchapter-078
  606. unification problemchapter-078
  607. case treechapter-078
  608. validchapter-078
  609. projection fragmentchapter-079
  610. regular descriptionchapter-080
  611. least fixed pointchapter-080
  612. D-algebrachapter-080
  613. applicative traversal interfacechapter-080
  614. containerchapter-081
  615. extensionchapter-081
  616. container morphismchapter-081
  617. indexed containerchapter-081
  618. ornamentchapter-081
  619. algebraic ornamentchapter-081
  620. accessiblechapter-082
  621. well foundedchapter-082
  622. well-founded recursorchapter-082
  623. measure relationchapter-082
  624. lexicographic relationchapter-082
  625. size-change labelchapter-083
  626. size-change matrixchapter-083
  627. truthfulchapter-083
  628. multipathchapter-083
  629. threadchapter-083
  630. size-change safechapter-083
  631. composition closurechapter-083
  632. idempotentchapter-083
  633. idempotent-cycle testchapter-083
  634. Mendler algebrachapter-084
  635. nested datatypechapter-084
  636. productivechapter-085
  637. streamchapter-085
  638. destructorschapter-085
  639. guarded corecursorchapter-085
  640. guarded-call invariantchapter-085
  641. observation depthchapter-085
  642. copatternchapter-085
  643. accepted by the guarded copattern fragmentchapter-085
  644. observationally equalchapter-085
  645. nested copatternchapter-085
  646. deep copatternchapter-085
  647. stream bisimulationchapter-085
  648. guard conditionchapter-086
  649. strong bisimulationchapter-086
  650. termination-sensitive weak equivalencechapter-086
  651. handlerchapter-086
  652. specificationchapter-087
  653. compositionally linearizablechapter-087
  654. interaction statechapter-088
  655. possibilitychapter-088
  656. possibility setchapter-088
  657. stablechapter-088
  658. PCUICchapter-089
  659. raw termschapter-089
  660. local declarationchapter-089
  661. global environmentchapter-089
  662. universe levelchapter-089
  663. universe constraintchapter-089
  664. parameterschapter-089
  665. indiceschapter-089
  666. constructor-uniformchapter-089
  667. singleton eliminationchapter-089
  668. extensional equality typechapter-090
  669. set modelchapter-090
  670. propositionchapter-090
  671. propositional truncationchapter-090
  672. Morita equivalentchapter-090
  673. computational conversionchapter-091
  674. partial equivalence relationchapter-091
  675. functionalchapter-091
  676. candidate type systemchapter-091
  677. evaluation saturationchapter-091
  678. closure inductionchapter-091
  679. closure derivationchapter-091
  680. unique valuationchapter-091
  681. demand–residual decompositionchapter-091
  682. realizeschapter-091
  683. pointwise functional contextschapter-091
  684. equal substitutionschapter-091
  685. locally similar for Γchapter-091
  686. admissible for a quotientchapter-091
  687. logic-enriched type theorychapter-092
  688. smallchapter-092
  689. very-dependent functionchapter-095
  690. Kleene trickchapter-096
  691. zero-cost castchapter-096
  692. zero-cost reusechapter-096
  693. λΠ-calculus modulo rewritingchapter-097
  694. parameter contextchapter-098
  695. shape operationchapter-098
  696. state–parameter modelchapter-098
  697. usage semiringchapter-099
  698. subjectchapter-100
  699. strong dependent tensorchapter-100
  700. quantitativechapter-100
  701. weak productchapter-100
  702. key redexchapter-100
  703. saturatedchapter-100
  704. statechapter-101
  705. heapchapter-101
  706. environmentchapter-101
  707. stackchapter-101
  708. multiplicitychapter-101
  709. well-resourcedchapter-101
  710. index-dependent choicechapter-102
  711. substitutionchapter-103
  712. dependent Boolean eliminationchapter-103
  713. observable effectchapter-103
  714. thunkable for Bchapter-103
  715. linear for M,Nchapter-103
  716. readerchapter-103
  717. stackchapter-103
  718. configurationchapter-103
  719. sensitive to a transitionchapter-103
  720. computational Sigma typechapter-103
  721. homomorphism termschapter-103
  722. monotonechapter-104
  723. conjunctivechapter-104
  724. verification conditionchapter-104
  725. representationchapter-104
  726. divergeschapter-105
  727. setoidchapter-105
  728. Kleisli arrowchapter-105
  729. partial-recursive presentationchapter-105
  730. finitarychapter-105
  731. context-wise reduction retractionchapter-106
  732. partial connectionchapter-106
  733. recursive object typechapter-107
  734. object valuechapter-107
  735. inert typechapter-107
  736. inertchapter-107
  737. tight typing judgmentchapter-107
  738. invertible typing judgmentchapter-107
  739. stable pathchapter-108
  740. singleton path typechapter-108
  741. negative-elimination-freechapter-109
  742. dependency listchapter-109
  743. continuation-passing translationchapter-109
  744. positive translationchapter-109
  745. trusted kernelchapter-110
  746. presyntaxchapter-110
  747. elaborationchapter-110
  748. bidirectional elaboration judgmentschapter-110
  749. canonical formschapter-111
  750. computability assignmentchapter-111
  751. atomchapter-111
  752. level normal formchapter-111
  753. equivalentchapter-111
  754. Root contractionchapter-111
  755. One-step reductionchapter-111
  756. head positionchapter-111
  757. head contextschapter-111
  758. weak-head stepchapter-111
  759. weak-head reductchapter-111
  760. Weak-head reductionchapter-111
  761. weak-head normal formchapter-111
  762. positivechapter-111
  763. stuckchapter-111
  764. normalization structurechapter-111
  765. environmentchapter-111
  766. identity environmentchapter-111
  767. semantic telescopechapter-111
  768. Ψ-admissiblechapter-111
  769. semantic substitutionchapter-111
  770. arbitrary source extensionchapter-111
  771. target weakeningchapter-111
  772. canonical liftchapter-111
  773. readback-defined fieldchapter-111
  774. support telescopechapter-111
  775. relational support telescopechapter-111
  776. relational world substitutionchapter-111
  777. natural dependent-family premisechapter-111
  778. stuckchapter-111
  779. peelingchapter-111
  780. generator orderchapter-111
  781. neutral casechapter-111
  782. realizing substitutionchapter-111
  783. related over Γ at Ψchapter-111
  784. valid over Γ in Δchapter-111
  785. contextual metavariablechapter-112
  786. metacontextchapter-112
  787. level metavariablechapter-112
  788. object constraintchapter-112
  789. formation guardchapter-112
  790. level constraintchapter-112
  791. constraint statechapter-112
  792. solutionchapter-112
  793. occurs checkchapter-112
  794. scope checkchapter-112
  795. Constraint generationchapter-112
  796. implicit saturationchapter-112
  797. level atomchapter-112
  798. canonical level normal formchapter-112
  799. stratified level problemchapter-112
  800. Weak-head normalizationchapter-112
  801. flexiblechapter-112
  802. rigidchapter-112
  803. flex–rigidchapter-112
  804. flex–flexchapter-112
  805. rigid–rigidchapter-112
  806. higher-order pattern occurrencechapter-112
  807. contextual pattern occurrencechapter-112
  808. direct contextual-pattern fragmentchapter-112
  809. rigidchapter-112
  810. solvedchapter-112
  811. ground-determination certificatechapter-112
  812. policy-alignedchapter-112
  813. policy-respecting elaborationchapter-112
  814. activechapter-112
  815. pattern substitutionchapter-112
  816. strongchapter-112
  817. shared term DAGchapter-113
  818. validchapter-113
  819. homogeneous closurechapter-113
  820. acyclic closurechapter-113
  821. linkschapter-113
  822. root classchapter-113
  823. goalchapter-114
  824. validationchapter-114
  825. contextual metavariablechapter-114
  826. proof statechapter-114
  827. tacticchapter-114
  828. closeschapter-114
  829. certified rewrite rulechapter-115
  830. terminating rewrite databasechapter-115
  831. respectfulchapter-115
  832. Zombiechapter-115
  833. core languagechapter-115
  834. surface languagechapter-115
  835. origin environmentchapter-116
  836. syntax objectchapter-116
  837. scoped expansion environmentchapter-116
  838. source environmentchapter-116
  839. generation timechapter-116
  840. inspection timechapter-116
  841. run timechapter-116
  842. valuationchapter-117
  843. ground elimination tablechapter-118
  844. constraint problemchapter-118
  845. solutionchapter-118
  846. StraTTchapter-118
  847. subStraTTchapter-118
  848. validchapter-118
  849. dominant ground substitutionchapter-118
  850. basic subtyping rule schematachapter-119
  851. coherence conditionschapter-119
  852. coercion signaturechapter-119
  853. declared-edge schematachapter-119
  854. cast programchapter-119
  855. parallel in Γchapter-119
  856. path coherentchapter-119
  857. description functoriality extensionchapter-120
  858. compacted neutralchapter-120
  859. base weak-head framechapter-120
  860. adapterchapter-120
  861. Timpl-clauseschapter-121
  862. first surviving rowchapter-121
  863. blocking patternchapter-121
  864. dependency preservingchapter-121
  865. simple clause matrixchapter-121
  866. constructor specializationchapter-121
  867. default matrixchapter-121
  868. readychapter-121
  869. written row mapchapter-121
  870. row-map invariantchapter-121
  871. clause matrixchapter-121
  872. frontier telescopechapter-121
  873. validchapter-121
  874. leaf equationchapter-121
  875. admissible constructor prefixchapter-121
  876. administrative translationchapter-121
  877. Timpl-datachapter-122
  878. Tfam-blockchapter-122
  879. hypothesis typechapter-122
  880. encoded empty typechapter-122
  881. dependency graphchapter-122
  882. strongly connected component (SCC)chapter-122
  883. strictly positivechapter-122
  884. Timpl-recchapter-123
  885. structural certificatechapter-123
  886. lexicographic certificatechapter-123
  887. Timpl-rec-corechapter-123
  888. function call graphchapter-123
  889. tagged block payloadchapter-123
  890. direct-child relationchapter-123
  891. program root contractionchapter-123
  892. dynamic compatible contextchapter-123
  893. Timpl-cochapter-124
  894. producerchapter-124
  895. head aliaschapter-124
  896. tail stepchapter-124
  897. observation wordchapter-124
  898. productivechapter-124
  899. guard-weighted call graphchapter-124
  900. Tcop-clausechapter-125
  901. Tcop-treechapter-125
  902. Tcop-corechapter-125
  903. typed copattern frontierchapter-125
  904. Texecchapter-126
  905. erasablechapter-126
  906. source data valueschapter-126
  907. relevance annotationchapter-126
  908. admissiblechapter-126
  909. representation well formedchapter-126
  910. runtime first orderchapter-126
  911. first-order map bodychapter-126
  912. Scheme0chapter-127
  913. static resultchapter-127
  914. dynamic resultchapter-127
  915. numeric call programchapter-127
  916. table prefixchapter-127
  917. completed offline specialization graphchapter-127
  918. power-site mapchapter-127
  919. configurationchapter-128
  920. progress guardchapter-128
  921. whistlechapter-128
  922. variantschapter-128
  923. homeomorphic embeddingchapter-128
  924. well-quasi-orderchapter-128
  925. most-specific generalizationchapter-128
  926. operational approximationchapter-128
  927. improvementchapter-128
  928. strong improvementchapter-128
  929. cost equivalencechapter-128
  930. admissiblechapter-128
  931. persistentchapter-129
  932. eliminablechapter-129
  933. persistent-value predicatechapter-129
  934. inversion-stable fragmentchapter-130
  935. binder-annotation erasurechapter-130
  936. word-parallel reductionchapter-130
  937. type variableschapter-131
  938. term variableschapter-131
  939. coercion constantschapter-131
  940. value type constructorschapter-131
  941. type functionschapter-131
  942. data constructorschapter-131
  943. top-level environmentchapter-131
  944. value typechapter-131
  945. consistentchapter-131
  946. homogeneouschapter-132
  947. joinablechapter-132
  948. CPS observation relationchapter-133
  949. component boundarychapter-133
  950. existential-closure calling interfacechapter-133
  951. isomorphicchapter-134
  952. compositionalchapter-135
  953. higher orderchapter-135
  954. closed under data flow to call siteschapter-135
  955. in defunctionalized formchapter-135
  956. Disentanglingchapter-135
  957. Merging apply functionschapter-135
  958. partial programchapter-136
  959. contextchapter-136
  960. trace propertychapter-136
  961. hyperpropertychapter-136
  962. behaviourchapter-136
  963. back-translationchapter-136
  964. full reflectionchapter-136
  965. universal embeddingchapter-136
  966. trace-based back-translationchapter-136
  967. Dynamic size matchingchapter-139
  968. Dynamic size checkingchapter-139
  969. consistentchapter-140
  970. positionchapter-140
  971. first orderchapter-140
  972. substitutionchapter-141
  973. categorychapter-141
  974. functorchapter-141
  975. productchapter-142
  976. pullbackchapter-142
  977. equalizerchapter-142
  978. conechapter-142
  979. limitchapter-142
  980. adjunctionchapter-142
  981. cartesian closedchapter-142
  982. slice categorychapter-142
  983. locally cartesian closedchapter-142
  984. Heyting algebrachapter-143
  985. Beck–Chevalley conditionchapter-143
  986. hyperdoctrinechapter-143
  987. comprehensionchapter-143
  988. first-order signaturechapter-143
  989. internal languagechapter-143
  990. Heyting pre-algebrachapter-144
  991. triposchapter-144
  992. generic predicatechapter-144
  993. partial applicative structurechapter-144
  994. P-valued setchapter-144
  995. functionalchapter-144
  996. proof-likechapter-145
  997. polechapter-145
  998. realizeschapter-145
  999. universal realizerchapter-145
  1000. identity-likechapter-145
  1001. valuationchapter-145
  1002. adequatechapter-145
  1003. substitution calculus over Schapter-146
  1004. category with familieschapter-146
  1005. Initialitychapter-146
  1006. uniform family of contextschapter-147
  1007. uniform family of typeschapter-147
  1008. uniform family of termschapter-147
  1009. presentationchapter-147
  1010. closurechapter-148
  1011. scoped algebrachapter-149
  1012. bracketingchapter-149
  1013. indexed comonadchapter-150
  1014. indexed lax monoidalchapter-150
  1015. indexed colax monoidalchapter-150
  1016. displayed CwFchapter-151
  1017. total modelchapter-151
  1018. groupoidchapter-152
  1019. smallchapter-152
  1020. familychapter-152
  1021. dependent objectchapter-152
  1022. display mapschapter-152
  1023. path objectchapter-152
  1024. isofibrationschapter-152
  1025. setoidchapter-153
  1026. extensional mapchapter-153
  1027. (m,n)-setoidchapter-153
  1028. n-setoidchapter-153
  1029. n-classoidchapter-153
  1030. familychapter-153
  1031. global elementchapter-153
  1032. partial equivalence relationchapter-153
  1033. domainchapter-153
  1034. familychapter-153
  1035. constantschapter-154
  1036. effect valueschapter-154
  1037. dcpochapter-154
  1038. dcppochapter-154
  1039. continuouschapter-154
  1040. strictchapter-154
  1041. continuous Σ-algebrachapter-154
  1042. algebraicchapter-154
  1043. pre-domainchapter-155
  1044. domainchapter-155
  1045. continuouschapter-155
  1046. admissiblechapter-155
  1047. partial computationschapter-155
  1048. completechapter-155
  1049. admissiblechapter-155
  1050. monotonechapter-155
  1051. assemblychapter-155
  1052. realizerschapter-155
  1053. uniform family of complete monotone PERschapter-155
  1054. comprehension categorychapter-156
  1055. splitchapter-156
  1056. fullchapter-156
  1057. types over Γchapter-156
  1058. display mapchapter-156
  1059. display mapchapter-156
  1060. identity typechapter-156
  1061. choicechapter-156
  1062. strictly stablechapter-156
  1063. weakly stablechapter-156
  1064. has weakly stable identity typeschapter-156
  1065. dependent exponentialchapter-156
  1066. arenachapter-157
  1067. moveschapter-157
  1068. enablingchapter-157
  1069. initialchapter-157
  1070. justified sequencechapter-157
  1071. P-viewchapter-157
  1072. O-viewchapter-157
  1073. playchapter-157
  1074. strategychapter-157
  1075. even-prefix closedchapter-157
  1076. deterministicchapter-157
  1077. interaction sequencechapter-157
  1078. innocentchapter-157
  1079. view functionchapter-157
  1080. contextchapter-158
  1081. compactchapter-158
  1082. tensorchapter-159
  1083. monoidal categorychapter-159
  1084. braidingchapter-159
  1085. symmetrychapter-159
  1086. symmetric monoidal categorychapter-159
  1087. signaturechapter-159
  1088. diagramchapter-159
  1089. boxeschapter-159
  1090. wiringchapter-159
  1091. equalchapter-159
  1092. closedchapter-159
  1093. linear–nonlinear adjunctionchapter-159
  1094. lax monoidalchapter-159
  1095. oplaxchapter-159
  1096. strongchapter-159
  1097. lockedchapter-160
  1098. CwDRAchapter-160
  1099. mode theorychapter-160
  1100. modeschapter-160
  1101. modalitieschapter-160
  1102. lockchapter-160
  1103. reflective subuniversechapter-160
  1104. signaturechapter-161
  1105. canonicitychapter-161
  1106. global-sections functorchapter-161
  1107. gluing categorychapter-161
  1108. syntactic projectionchapter-161
  1109. phase separatedchapter-161
  1110. propositionchapter-161
  1111. open modalitychapter-161
  1112. closed modalitychapter-161
  1113. open-modalchapter-161
  1114. closed-modalchapter-161
  1115. partial element typechapter-161
  1116. extent typechapter-161
  1117. realignment structurechapter-161
  1118. strongchapter-161
  1119. strict glue typechapter-161
  1120. delayed substitutionchapter-162
  1121. defined by guarded recursionchapter-162
  1122. L"ob inductionchapter-162
  1123. guarded stream typechapter-162
  1124. topos of treeschapter-162
  1125. restriction mapschapter-162
  1126. contractivechapter-162
  1127. witnesschapter-162
  1128. kth observationchapter-162
  1129. clock contextchapter-162
  1130. clock irrelevancechapter-162
  1131. predicatechapter-163
  1132. later operatorchapter-163
  1133. configurationchapter-163
  1134. convergeschapter-163
  1135. ω-cpochapter-163
  1136. pointedchapter-163
  1137. continuouschapter-163
  1138. relation environmentchapter-164
  1139. relational translationchapter-164
  1140. satisfies identity extensionchapter-164
  1141. size variableschapter-165
  1142. size expressionchapter-165
  1143. extended size expressionchapter-165
  1144. measurechapter-165
  1145. size contextchapter-165
  1146. polaritychapter-165
  1147. normalized successorchapter-165
  1148. valuationchapter-165
  1149. satisfieschapter-165
  1150. Kindschapter-165
  1151. varianceschapter-165
  1152. variant rowchapter-165
  1153. record rowchapter-165
  1154. measured typechapter-165
  1155. constrained typechapter-165
  1156. mutual blockchapter-165
  1157. constrained typechapter-165
  1158. terminally stuckchapter-165
  1159. neutralchapter-165
  1160. simulateschapter-165
  1161. reducibility candidatechapter-165
  1162. smallchapter-166
  1163. largechapter-166
  1164. contractiblechapter-166
  1165. impredicativechapter-166
  1166. endofunctorchapter-166
  1167. size-indexed small typechapter-166
  1168. F-algebrachapter-166
  1169. initialchapter-166
  1170. size-indexed F-algebrachapter-166
  1171. weakly commutes with the existentialchapter-166
  1172. F-coalgebrachapter-166
  1173. terminalchapter-166
  1174. weakly commutes with the universalchapter-166
  1175. assemblychapter-166
  1176. realizeschapter-166
  1177. trackschapter-166
  1178. modestchapter-166
  1179. partial equivalence relationchapter-166
  1180. logical spanschapter-167
  1181. core theorychapter-167
  1182. legschapter-167
  1183. unarychapter-167
  1184. binarychapter-167
  1185. global theorychapter-167
  1186. local theorychapter-167
  1187. gluing modelchapter-167
  1188. substitutionchapter-168
  1189. exhaustivechapter-168
  1190. co-exhaustivechapter-168
  1191. backwardchapter-168
  1192. tracechapter-168
  1193. lenschapter-169
  1194. lawfulchapter-169
  1195. put-getchapter-169
  1196. get-putchapter-169
  1197. put-putchapter-169
  1198. prismchapter-169
  1199. lawfulchapter-169
  1200. traversalchapter-169
  1201. profunctorchapter-169
  1202. Tambara structurechapter-169
  1203. dinatural transformationchapter-169
  1204. endchapter-169
  1205. coendchapter-169
  1206. monoidal actionchapter-169
  1207. residualchapter-169
  1208. lawfulchapter-169
  1209. setterchapter-169
  1210. dependent lenschapter-170
  1211. B-indexed categorychapter-170
  1212. representativechapter-170
  1213. D-valued Tambara representationchapter-170
  1214. pPCFchapter-171
  1215. weak-normalchapter-171
  1216. stochasticchapter-171
  1217. result distributionchapter-171
  1218. probabilistic coherence spacechapter-171
  1219. depends on at most n parameterschapter-171
  1220. finite subdistributionchapter-172
  1221. tracechapter-172
  1222. σ-algebrachapter-172
  1223. measurable spacechapter-172
  1224. measurablechapter-172
  1225. measurechapter-172
  1226. subprobability measurechapter-172
  1227. Dirac measurechapter-172
  1228. kernelchapter-172
  1229. return kernelchapter-172
  1230. bindchapter-172
  1231. samplerchapter-172
  1232. pushforward measurechapter-172
  1233. computable metric spacechapter-172
  1234. computable distributionchapter-172
  1235. samplablechapter-172
  1236. conditional distributionchapter-173
  1237. computablechapter-173
  1238. computable Polish spacechapter-173
  1239. computablechapter-173
  1240. P-almost computablechapter-173
  1241. P-almost decidablechapter-173
  1242. conditioning operatorchapter-173
  1243. quasi-Borel spacechapter-174
  1244. random elementschapter-174
  1245. morphismchapter-174
  1246. probability measurechapter-174
  1247. ω-quasi-Borel spacechapter-174
  1248. statistical powerdomainchapter-174
  1249. SFPCchapter-174
  1250. discrete inference representationchapter-175
  1251. meaning functionschapter-175
  1252. discrete inference transformationchapter-175
  1253. inference transformerchapter-175
  1254. enriched expressionschapter-176
  1255. stuckchapter-178
  1256. error creditchapter-178
  1257. credit derivationchapter-178
  1258. stock measurechapter-179
  1259. deterministicchapter-179
  1260. quasi-Borel familychapter-180
  1261. fibred random elementschapter-180
  1262. map of familieschapter-180
  1263. comprehensionchapter-180
  1264. simple termschapter-181
  1265. partial derivativechapter-181
  1266. simple resource termschapter-181
  1267. poly-termschapter-181
  1268. resource termchapter-181
  1269. uniformchapter-181
  1270. B"ohm treechapter-181
  1271. tangent representationchapter-182
  1272. backpropagatorchapter-183
  1273. qubit statechapter-184
  1274. n-qubit register statechapter-184
  1275. unitarychapter-184
  1276. Measuringchapter-184
  1277. density matrixchapter-184
  1278. partial tracechapter-184
  1279. channelchapter-184
  1280. program statechapter-184
  1281. linking functionchapter-184
  1282. well typed of type Bchapter-184
  1283. error statechapter-184
  1284. skeletonchapter-184
  1285. decorationchapter-184
  1286. symmetric monoidal categorychapter-184
  1287. compact closedchapter-184
  1288. daggerchapter-184
  1289. dagger compactchapter-184
  1290. wire type constantschapter-185
  1291. parameter typeschapter-185
  1292. simple typeschapter-185
  1293. labelschapter-185
  1294. boxed circuitchapter-185
  1295. label contextchapter-185
  1296. configurationchapter-185
  1297. labelled circuitschapter-185
  1298. well typed with input labels Q, output labels Q', and type Achapter-185
  1299. parameter termschapter-186
  1300. indiceschapter-186
  1301. parameter contextchapter-186
  1302. shapechapter-186
  1303. topologychapter-187
  1304. open setschapter-187
  1305. topological spacechapter-187
  1306. neighborhoodchapter-187
  1307. continuouschapter-187
  1308. homeomorphismchapter-187
  1309. connectedchapter-187
  1310. compactchapter-187
  1311. Hausdorffchapter-187
  1312. pathchapter-187
  1313. loopchapter-187
  1314. concatenationchapter-187
  1315. reversalchapter-187
  1316. homotopychapter-187
  1317. path homotopychapter-187
  1318. homotopy equivalencechapter-187
  1319. homotopy equivalentchapter-187
  1320. contractiblechapter-187
  1321. deformation retractionchapter-187
  1322. pointed spacechapter-187
  1323. loop spacechapter-187
  1324. disjoint unionchapter-187
  1325. pushoutchapter-187
  1326. wedgechapter-187
  1327. conechapter-187
  1328. suspensionchapter-187
  1329. mapping conechapter-187
  1330. standard n-simplexchapter-187
  1331. covering mapchapter-188
  1332. evenly coveredchapter-188
  1333. fiberchapter-188
  1334. homotopy lifting propertychapter-188
  1335. Serre fibrationchapter-188
  1336. Hurewicz fibrationchapter-188
  1337. path spacechapter-189
  1338. whiskeringschapter-189
  1339. homotopychapter-189
  1340. mere propositionchapter-189
  1341. setchapter-189
  1342. simplex categorychapter-190
  1343. simplicial setchapter-190
  1344. facechapter-190
  1345. degeneracychapter-190
  1346. degeneratechapter-190
  1347. k-hornchapter-190
  1348. Kan fibrationchapter-190
  1349. Kan complexchapter-190
  1350. simplicial homotopychapter-190
  1351. Univalencechapter-193
  1352. comparison mapchapter-193
  1353. univalent universechapter-193
  1354. univalence mapchapter-193
  1355. n-typechapter-195
  1356. circlechapter-198
  1357. higher inductive typechapter-198
  1358. dependent pathchapter-198
  1359. pointed mapchapter-202
  1360. zero mapchapter-202
  1361. n-th homotopy groupchapter-202
  1362. precategorychapter-207
  1363. univalent categorychapter-207
  1364. cardinalchapter-210
  1365. accessibility witnesschapter-210
  1366. ordinalchapter-210
  1367. Dedekind cutchapter-211
  1368. roundednesschapter-211
  1369. Cauchy approximationchapter-211
  1370. Observational equalitychapter-215
  1371. strict proposition sortschapter-215
  1372. implicit universe annotationchapter-215
  1373. intervalchapter-217
  1374. dimension contextchapter-217
  1375. dimension substitutionchapter-217
  1376. diagonal cofibrationchapter-218
  1377. Cartesian intervalchapter-218
  1378. Cartesian cofibrationchapter-218
  1379. coercionchapter-218
  1380. homogeneous compositionchapter-218
  1381. shared term DAGappendix-rules-057
  1382. validappendix-rules-057
  1383. homogeneous closureappendix-rules-057
  1384. acyclic closureappendix-rules-057
  1385. linksappendix-rules-057
  1386. root classappendix-rules-057
  1387. de Bruijn indexappendix-tutorials-001

Search the book

Type to search the local edition.