We develop the Scott model of the programming language PCF in constructive predicative univalent type theory. To account for the non-termination in PCF, we work with the partial map classifier monad (also known as the lifting monad) from topos theory, which has been extended to constructive type theory by Knapp and Escardo. Our results show that lifting is a viable approach to partiality in univalent type theory. Moreover, we show that the Scott model can be constructed in a predicative and constructive setting. Other approaches to partiality either require some form of choice or higher inductive-inductive types. We show that one can do without these extensions.
Capretta's delay monad has been used to give a constructive approach to domain theory @cite_9 . However, the objects have the wrong equality'', so that every object comes with an equivalence relation that maps must preserve. The framework of univalent mathematics in which we have placed our development provides a more natural approach. Moreover, we do not make use of Coq's impredicative Prop universe and our treatment incorporates directed complete posets (dcpos) and not just @math -cpos.
@cite_9
2963889233 2565502105 1813662263 2748981990
Capretta's delay monad can be used to model partial computations, but it has the wrong'' notion of built-in equality, strong bisimilarity. An alternative is to quotient the delay monad by the right''notion of equality, weak bisimilarity. However, recent work by suggests that it is impossible to define a monad structure on the resulting construction in common forms of type theory without assuming (instances of) the axiom of countable choice. Using an idea from homotopy type theory---a higher inductive-inductive type---we construct a partiality monad without relying on countable choice. We prove that, in the presence of countable choice, our partiality monad is equivalent to the delay monad quotiented by weak bisimilarity. Furthermore we outline several applications. A family of syntactic models for the calculus of construction with universes (CCω) is described, all of them preserving conversion of the calculus definitionally, and thus giving rise directly to a program transformation of CCω into itself. Those models are based on the remark that negative type constructors (e.g. dependent product, coinductive types or universes) are underspecified in type theory-which leaves some freedom on extra intensional specifications. The model construction can be seen as a compilation phase from a complex type theory into a simpler type theory. Such models can be used to derive (the negative part of) independence results with respect to CCω, such as functional extensionality, propositional extensionality, univalence or the fact that bisimulation on a coinductive type may not coincide with equality. They can also be used to add new principles to the theory, which we illustrate by defining a version of CCω with ad-hoc polymorphism that shows in particular that parametricity is not an implicit requirement of type theory. The correctness of some of the models program transformations have been checked in the Coq proof assistant and have been instrumented as a Coq plugin. We present a Coq formalization of constructive *** -cpos (extending earlier work by Paulin-Mohring) up to and including the inverse-limit construction of solutions to mixed-variance recursive domain equations, and the existence of invariant relations on those solutions. We then define operational and denotational semantics for both a simply-typed CBV language with recursion and an untyped CBV language, and establish soundness and adequacy results in each case. We formalise the axiomatic set theory second-order ZF in the constructive type theory of Coq assuming excluded middle. In this setting we prove Zermelo’s embedding theorem for models, categoricity in all cardinalities, and the correspondence of inner models and Grothendieck universes. Our results are based on an inductive definition of the cumulative hierarchy eliminating the need for ordinals and transfinite recursion.