The denotational semantics of programming languages

1976 ◽  
Vol 19 (8) ◽  
pp. 437-453 ◽  
Author(s):  
R. D. Tennent
1993 ◽  
Vol 3 (2) ◽  
pp. 137-159 ◽  
Author(s):  
Manfred Droste ◽  
Rüdiger Gübel

In the theory of denotational semantics of programming languages, several authors have constructed various kinds of universal domains. We present here a categorical generalization of a well-known result in model theory, which we use to characterize large classes of reasonable categories that contain universal homogeneous objects. The existence of such objects is characterized by the condition that the finite objects in the category satisfy the amalgamation property. We derive from this the existence and uniqueness of universal homogeneous domains for several categories of bifinite domains, with embedding-projection-pairs as morphisms. We also obtain universal homogeneous objects for various categories of stable bifinite domains. In contrast, several categories of event domains and concrete domains and the category of all coherent Scott-domains do not contain universal homogeneous objects. Finally, we show that all our constructions can be performed effectively.


1990 ◽  
Vol 01 (04) ◽  
pp. 413-424 ◽  
Author(s):  
MANFRED DROSTE ◽  
RÜDIGER GÖBEL

In the theory of denotational semantics of programming languages, several authors proved the existence of particular kinds of universal domains. D. Scott constructed universal information systems, which are, however, not unique up to isomorphism. Here, we use a model-theoretic technique to establish the existence and uniqueness of a universal homogeneous information system. Similar results are also obtained for canonical and for stable information systems, respectively.


2018 ◽  
Vol 29 (3) ◽  
pp. 465-510 ◽  
Author(s):  
RASMUS E. MØGELBERG ◽  
MARCO PAVIOTTI

Just like any other branch of mathematics, denotational semantics of programming languages should be formalised in type theory, but adapting traditional domain theoretic semantics, as originally formulated in classical set theory to type theory has proven challenging. This paper is part of a project on formulating denotational semantics in type theories with guarded recursion. This should have the benefit of not only giving simpler semantics and proofs of properties such as adequacy, but also hopefully in the future to scale to languages with advanced features, such as general references, outside the reach of traditional domain theoretic techniques.Working inGuarded Dependent Type Theory(GDTT), we develop denotational semantics for Fixed Point Calculus (FPC), the simply typed lambda calculus extended with recursive types, modelling the recursive types of FPC using the guarded recursive types ofGDTT. We prove soundness and computational adequacy of the model inGDTTusing a logical relation between syntax and semantics constructed also using guarded recursive types. The denotational semantics is intensional in the sense that it counts the number of unfold-fold reductions needed to compute the value of a term, but we construct a relation relating the denotations of extensionally equal terms, i.e., pairs of terms that compute the same value in a different number of steps. Finally, we show how the denotational semantics of terms can be executed inside type theory and prove that executing the denotation of a boolean term computes the same value as the operational semantics of FPC.


2004 ◽  
Vol 11 (22) ◽  
Author(s):  
Gian Luca Cattani ◽  
Glynn Winskel

This paper studies fundamental connections between profunctors (i.e., distributors, or bimodules), open maps and bisimulation. In particular, it proves that a colimit preserving functor between presheaf categories (corresponding to a profunctor) preserves open maps and open map bisimulation. Consequently, the composition of profunctors preserves open maps as 2-cells. A guiding idea is the view that profunctors, and colimit preserving functors, are linear maps in a model of classical linear logic. But profunctors, and colimit preserving functors, as linear maps, are too restrictive for many applications. This leads to a study of a range of pseudo-comonads and how non-linear maps in their co-Kleisli bicategories preserve open maps and bisimulation. The pseudo-comonads considered are based on finite colimit completion, ``lifting'', and indexed families. The paper includes an appendix summarising the key results on coends, left Kan extensions and the preservation of colimits. One motivation for this work is that it provides a mathematical framework for extending domain theory and denotational semantics of programming languages to the more intricate models, languages and equivalences found in concurrent computation. But the results are likely to have more general applicability because of the ubiquitous nature of profunctors.


1989 ◽  
Vol 18 (298) ◽  
Author(s):  
Guo Qiang Zhang

<p>This dissertation studies the logical aspects of domains as used in the denotational semantics of programming languages. Frameworks of domain logics are introduced which serve as basic tools for the systematic derivation of proof systems from the denotational semantics of programming languages. The proof systems so derived are guaranteed to agree with the denotational semantics in the sense that the denotation of any program coincides with the set of assertations true of it.</p><p>The study focuses on two frameworks for denotational semantics: the <strong>sep</strong> domains, and the less standard, but important, category of dI-domains with stable functions</p>


1997 ◽  
Vol 7 (5) ◽  
pp. 453-468 ◽  
Author(s):  
JOHN POWER ◽  
EDMUND ROBINSON

We introduce the notions of premonoidal category and premonoidal functor, and show how these can be used in the denotational semantics of programming languages. We characterize the semantic definitions of Eugenio Moggi's monads as notions of computation, exhibit a representation theorem for our premonoidal setting in terms of monads, and give a fibrational setting for the structure.


2003 ◽  
Vol 9 (2) ◽  
pp. 169-180 ◽  
Author(s):  
P.-L. Curien

AbstractWe recall some of the early occurrences of the notions of interactivity and symmetry in the operational and denotational semantics of programming languages. We suggest some connections with ludics.


Sign in / Sign up

Export Citation Format

Share Document