The Scott model of PCF in univalent type theory T1VFA7TXPA

URI	`m2://res/T1VFA7TXPA`
Kind	preprint
Creators	Tom de Jong
Date	2019-04-22
MSC	03-XX
Subjects	arxiv math.LO, arxiv cs.LO
Scope	in

Expressions

e1: version, preprint

Language	en
Date	2019-04-22
Ids	arXiv 1904.09810

Items in this resource

The mentions of the inventory that name this resource. Each name links to the card of its inventory row.

Item	Kind	Where	Source
\coqident{MoreFoundations}{Wtypes}{picompact_empty}, \coqident{MoreFoundations}{Wtypes}{picompact_unit	example	example 65	arxiv
Jasper Hugunin	statement	theorem 73	arxiv
\coqident{Partiality}{PartialElements}{liftorder_least	definition	definition 19	arxiv
22Z3R9KWHR	statement	proposition 40	arxiv
27A5Q75YZZ	statement	lemma 79	arxiv
2CYNRV5PWS	statement	lemma 76	arxiv
\coqident{MoreFoundations}{Wtypes}{subtrees	definition	definition 75	arxiv
3BSNGX4B6A	statement	theorem 25	arxiv
Theorem 5.8 in , Section 2.2	statement	theorem 24	arxiv
3J88CXDDTZ	statement	theorem 13	arxiv
\coqident{Algebra}{DCPO}{dcpowithbottom	definition	definition 14	arxiv
4FP7A70EWK	definition	definition 68	arxiv
4PRYN08A2A	statement	lemma 11	arxiv
4T68W3XY85	definition	definition 50	arxiv
5F0WMFZQ2S	statement	lemma 36	arxiv
\coqident{Partiality}{PartialElements}{lift_embedding	definition	definition 20	arxiv
\coqident{Partiality}{PCF}{numeral	definition	definition 32	arxiv
\coqident{MoreFoundations}{ClosureOfHrel}{refl_trans_clos}, \coqident{MoreFoundations}{ClosureOfHrel}{refl_trans_clos_hrel	definition	definition 35	arxiv
\coqident{Partiality}{PartialElements}{lift	definition	definition 18	arxiv
8N7QQZA78X	statement	lemma 47	arxiv
\coqident{MoreFoundations}{ClosureOfHrel}{refltransclos_step}, \coqident{MoreFoundations}{ClosureOfHrel}{refltransclos_step_hrel	definition	definition 55	arxiv
\coqident{Foundations}{Sets}{posetmorphism	definition	definition 4	arxiv
9Y20H0KX3Z	statement	theorem	arxiv
\coqident{MoreFoundations}{Wtypes}{getfib	definition	definition 77	arxiv
A332XXR2T1	statement	theorem 15	arxiv
AGNA86SD57	statement	lemma 57	arxiv
AQG9SSB64V	statement	theorem 16	arxiv
ASCGEPCYSG	example	example 1	arxiv
\coqident{Partiality}{LiftMonad}{Kleisli_extension	definition	definition 23	arxiv
\coqident{Foundations}{Sets}{PartialOrder	definition	definition 2	arxiv
\coqident{MoreFoundations}{ClosureOfHrel}{isdecidable_hrel	definition	definition 59	arxiv
\coqident{Foundations}{Sets}{hrel	definition	definition 54	arxiv
EM97S40JFG	statement	lemma 17	arxiv
\coqident{Algebra}{DCPO}{isupperbound}, \coqident{Algebra}{DCPO}{islub}, \coqident{Algebra}{DCPO}{isdirectedcomplete	definition	definition 7	arxiv
\coqident{Partiality}{PCF}{denotational_semantics_terms	definition	definition 38	arxiv
FFGK1SRFF6	statement	lemma 45	arxiv
FWAHSDETXG	example	example 63	arxiv
\coqident{Partiality}{PartialElements}{isdefined}, \coqident{Partiality}{PartialElements}{value	definition	definition 21	arxiv
GGA66QW44D	statement	lemma 78	arxiv
GM5TPKCVZN	statement	lemma 46	arxiv
\coqident{Partiality}{PCF}{type	definition	definition 30	arxiv
J6KVJYHPJJ	statement	lemma 51	arxiv
JFSYR5Y2BG	statement	lemma 69	arxiv
\coqident{Partiality}{PCF}{smallstep'}, \coqident{Partiality}{PCF}{smallstep	definition	definition 33	arxiv
JWTCVCYYE4	statement	lemma 44	arxiv
\coqident{Algebra}{DCPO}{isdcpomorphism	definition	definition 10	arxiv
KWVF33GJMJ	statement	lemma 56	arxiv
\coqident{Partiality}{PCF}{adequacy_relation	definition	definition 43	arxiv
MQ2SDDHGWG	statement	theorem 27	arxiv
cf.\ Theorem 5.14 in and Theorem 1	statement	theorem 26	arxiv
N9PMCV182A	statement	theorem 66	arxiv
\coqident{MoreFoundations}{Wtypes}{indexedWtype	definition	definition 62	arxiv
Q4P2B7BENJ	statement	lemma 12	arxiv
Soundness	statement	theorem 41	arxiv
QNH5755194	statement	lemma 22	arxiv
\coqident{Partiality}{PCF}{denotational_semantics_type	definition	definition 37	arxiv
RBWXNPK81W	statement	theorem 80	arxiv
\coqident{Partiality}{PCF}{term	definition	definition 31	arxiv
RW4SSP6PEB	statement	lemma 48	arxiv
Definition 2.4.2 in , \coqident{Foundations}{PartA}{hfiber	definition	definition 72	arxiv
T6E517A122	statement	lemma 52	arxiv
TQAJKCQ0DJ	statement	theorem 71	arxiv
Computational adequacy	statement	theorem 42	arxiv
VVYVCJ108T	statement	lemma 70	arxiv
\texttt{WeaklyCompactTypes} in , \coqident{MoreFoundations}{Wtypes}{picompact	definition	definition 64	arxiv
WG7TZRVCMC	statement	lemma 67	arxiv
\coqident{MoreFoundations}{ClosureOfHrel}{is_singlevalued	definition	definition 58	arxiv
X3BQCGAPH0	statement	lemma 60	arxiv
\coqident{Algebra}{DCPO}{isdirected	definition	definition 5	arxiv
XX9FQDKDHM	statement	theorem 53	arxiv
Fundamental Theorem	statement	lemma 49	arxiv
ZQKBRDJS5J	statement	lemma 74	arxiv

Catalogue records

arxiv: 1904.09810 (work)
arxiv_text: 1904.09810 (work)