scholarly journals Domain Theory for Concurrency

2003 ◽  
Vol 10 (43) ◽  
Author(s):  
Mikkel Nygaard ◽  
Glynn Winskel
Keyword(s):  
Linear Logic ◽  
Operational Semantics ◽  
Denotational Semantics ◽  
Higher Order ◽  
The Other ◽  
Domain Theory ◽  
Parallel Composition ◽  
Concurrent Computation ◽  
Contextual Equivalence

A simple domain theory for concurrency is presented. Based on a categorical model of linear logic and associated comonads, it highlights the role of linearity in concurrent computation. Two choices of comonad yield two expressive metalanguages for higher-order processes, both arising from canonical constructions in the model. Their denotational semantics are fully abstract with respect to contextual equivalence. One language derives from an exponential of linear logic; it supports a straightforward operational semantics with simple proofs of soundness and adequacy. The other choice of comonad yields a model of affine-linear logic, and a process language with a tensor operation to be understood as a parallel composition of independent processes. The domain theory can be generalised to presheaf models, providing a more refined treatment of nondeterministic branching. The article concludes with a discussion of a broader programme of research, towards a fully fledged domain theory for concurrency.

scholarly journals A Presheaf Semantics of Value-Passing Processes

1996 ◽  
Vol 3 (44) ◽  
Author(s):  
Glynn Winskel
Keyword(s):  
Operational Semantics ◽  
Denotational Semantics ◽  
Domain Theory ◽  
Process Calculi ◽  
Traditional Definition ◽  
Open Maps

This paper investigates presheaf models for process calculi with<br />value passing. Denotational semantics in presheaf models are shown<br />to correspond to operational semantics in that bisimulation obtained<br />from open maps is proved to coincide with bisimulation as defined<br />traditionally from the operational semantics. Both "early" and "late"<br />semantics are considered, though the more interesting "late" semantics<br />is emphasised. A presheaf model and denotational semantics is proposed<br />for a language allowing process passing, though there remains<br />the problem of relating the notion of bisimulation obtained from open<br />maps to a more traditional definition from the operational semantics.<br />A tentative beginning is made of a "domain theory" supporting<br />presheaf models.

Same stimuli, same subjects, different perception

2018 ◽  
Vol 4 (2) ◽  
pp. 231-252
Author(s):  
Marjoleine Sloos ◽  
Wang Lei
Keyword(s):  
Speech Perception ◽  
Higher Order ◽  
The Other ◽  
Linguistic Knowledge ◽  
Lexical Tone ◽  
Biased Perception

Abstract Believed dialect influences speech perception by linguistically naïve speakers. How much accent-induced bias affects perception of linguistically trained speakers is still unclear. This study experimentally investigates the influence of believed dialect on plosive perception by subjects who were phonetically and phonologically trained. Identical syllables were presented twice to each subject. In one session, the subjects were informed that the variety was a Mandarin dialect which has voiceless unaspirated and aspirated voiceless stops; and in the other session that it was a Wu dialect, which has voiceless unaspirated, voiceless aspirated, and breathy stops. More breathy stops were reported if Wu was the believed dialect. Plosive phonation in Wu is related to lexical tone, and we show that lexical tone causes another bias to plosive perception. This suggests that linguistically trained transcribers are susceptible to higher order linguistic knowledge and it demonstrates the difficulty of avoiding biased perception when the coder forms a belief about the variety that he/she transcribes. We also advocate speech perception models which include a component that accounts for the role of expected sounds.

Mechanizing proofs with logical relations – Kripke-style

2018 ◽  
Vol 28 (9) ◽  
pp. 1606-1638 ◽  
Author(s):  
ANDREW CAVE ◽  
BRIGITTE PIENTKA
Keyword(s):  
Case Studies ◽  
Operational Semantics ◽  
Lambda Calculus ◽  
Equational Theory ◽  
Higher Order ◽  
Abstract Syntax ◽  
Completeness Proof ◽  
Typed Lambda Calculus ◽  
Contextual Equivalence ◽  
The Right

Proofs with logical relations play a key role to establish rich properties such as normalization or contextual equivalence. They are also challenging to mechanize. In this paper, we describe two case studies using the proof environmentBeluga: First, we explain the mechanization of the weak normalization proof for the simply typed lambda-calculus; second, we outline how to mechanize the completeness proof of algorithmic equality for simply typed lambda-terms where we reason about logically equivalent terms. The development of these proofs inBelugarelies on three key ingredients: (1) we encode lambda-terms together with their typing rules, operational semantics, algorithmic and declarative equality using higher order abstract syntax (HOAS) thereby avoiding the need to manipulate and deal with binders, renaming and substitutions, (2) we take advantage ofBeluga's support for representing derivations that depend on assumptions and first-class contexts to directly state inductive properties such as logical relations and inductive proofs, (3) we exploitBeluga's rich equational theory for simultaneous substitutions; as a consequence, users do not need to establish and subsequently use substitution properties, and proofs are not cluttered with references to them. We believe these examples demonstrate thatBelugaprovides the right level of abstractions and primitives to mechanize challenging proofs using HOAS encodings. It also may serve as a valuable benchmark for other proof environments.

scholarly journals HOPLA--A Higher-Order Process Language

2002 ◽  
Vol 9 (49) ◽  
Author(s):  
Mikkel Nygaard ◽  
Glynn Winskel
Keyword(s):  
Operational Semantics ◽  
Lambda Calculus ◽  
Expressive Power ◽  
Higher Order ◽  
Domain Theory ◽  
Order Process ◽  
Encode Process ◽  
Mobile Ambients ◽  
Computation Path ◽  
Congruence Properties

A small but powerful language for higher-order nondeterministic processes is introduced. Its roots in a linear domain theory for concurrency are sketched though for the most part it lends itself to a more operational account. The language can be viewed as an extension of the lambda calculus with a ``prefixed sum'', in which types express the form of computation path of which a process is capable. Its operational semantics, bisimulation, congruence properties and expressive power are explored; in particular, it is shown how it can directly encode process languages such as CCS, CCS with process passing, and mobile ambients with public names.

scholarly journals New-HOPLA--A Higher-Order Process Language with Name Generation

2004 ◽  
Vol 11 (21) ◽  
Author(s):  
Glynn Winskel ◽  
Francesco Zappa Nardelli
Keyword(s):  
Operational Semantics ◽  
Expressive Power ◽  
Higher Order ◽  
Domain Theory ◽  
Process Algebras ◽  
Order Process ◽  
Pi Calculus ◽  
Mobile Ambients ◽  
Congruence Properties

This paper introduces new-HOPLA, a concise but powerful language for higher-order nondeterministic processes with name generation. Its origins as a metalanguage for domain theory are sketched but for the most part the paper concentrates on its operational semantics. The language is typed, the type of a process describing the shape of the computation paths it can perform. Its transition semantics, bisimulation, congruence properties and expressive power are explored. Encodings are given of well-known process algebras, including pi-calculus, Higher-Order pi-calculus and Mobile Ambients.

A Linear Metalanguage for Concurrency

1998 ◽  
Vol 5 (31) ◽  
Author(s):  
Glynn Winskel
Keyword(s):  
Linear Logic ◽  
Higher Order ◽  
The Other ◽  
Order Process ◽  
Open Problems ◽  
Concurrent Process ◽  
Open Map ◽  
Pi Calculus ◽  
Categorical Models ◽  
Future Work

A metalanguage for concurrent process languages is introduced.<br />Within it a range of process languages can be defined, including<br />higher-order process languages where processes are passed and received as arguments. (The process language has, however, to be linear, in the sense that a process received as an argument can be run at most once, and not include name generation as in the Pi-Calculus.) The metalanguage is provided with two interpretations both of which can be understood as categorical models of a variant of linear logic. One interpretation is in a<br />simple category of nondeterministic domains; here a process will denote its set of traces. The other interpretation, obtained by direct analogy with the nondeterministic domains, is in a category of presheaf categories; the nondeterministic branching behaviour of a process is captured in its denotation as a presheaf. Every presheaf category possesses a notion of (open-map) bisimulation, preserved by terms of the metalanguage. The<br />conclusion summarises open problems and lines of future work.

Contextual equivalence for inductive definitions with binders in higher order typed functional programming

2013 ◽  
Vol 23 (6) ◽  
pp. 658-700
Author(s):  
MATTHEW R. LAKIN ◽  
ANDREW M. PITTS
Keyword(s):  
Functional Programming ◽  
Operational Semantics ◽  
Higher Order ◽  
European Symposium ◽  
Proof Search ◽  
Inductive Definitions ◽  
University Of Cambridge ◽  
Meta Programming ◽  
Contextual Equivalence ◽  
Phd Thesis

AbstractCorrect handling of names and binders is an important issue in meta-programming. This paper presents an embedding of constraint logic programming into the αML functional programming language, which provides a provably correct means of implementing proof search computations over inductive definitions involving names and binders modulo α-equivalence. We show that the execution of proof search in the αML operational semantics is sound and complete with regard to the model-theoretic semantics of formulae, and develop a theory of contextual equivalence for the subclass of αML expressions which correspond to inductive definitions and formulae. In particular, we prove that αML expressions, which denote inductive definitions, are contextually equivalent precisely when those inductive definitions have the same model-theoretic semantics. This paper is a revised and extended version of the conference paper (Lakin, M. R. & Pitts, A. M. (2009) Resolving inductive definitions with binders in higher-order typed functional programming. InProceedings of the 18th European Symposium on Programming (ESOP 2009), Castagna, G. (ed), Lecture Notes in Computer Science, vol. 5502. Berlin, Germany: Springer-Verlag, pp. 47–61) and draws on material from the first author's PhD thesis (Lakin, M. R. (2010)An Executable Meta-Language for Inductive Definitions with Binders. University of Cambridge, UK).

scholarly journals A denotational semantics for the symmetric interaction combinators

2007 ◽  
Vol 17 (3) ◽  
pp. 527-562 ◽  
Author(s):  
DAMIANO MAZZA
Keyword(s):  
Linear Logic ◽  
Denotational Semantics ◽  
Distributed Computation ◽  
Higher Order ◽  
Parallel Execution ◽  
Turing Machines ◽  
Algebraic Semantics ◽  
Relational Semantics ◽  
Completeness Result ◽  
Higher Order Functions

The symmetric interaction combinators are a variant of Lafont's interaction combinators. They enjoy a weaker universality property with respect to interaction nets, but are equally expressive. They are a model of deterministic distributed computation and share the good properties of Turing machines (elementary reductions) and of the λ-calculus (higher-order functions and parallel execution). We introduce a denotational semantics for this system, which is inspired by the relational semantics for linear logic, and prove an injectivity and full completeness result for it. We also consider the algebraic semantics defined by Lafont, and prove that the two are strongly related.

An operational domain-theoretic treatment of recursive types

2013 ◽  
Vol 24 (1) ◽  
Author(s):  
WENG KIN HO
Keyword(s):  
Operational Semantics ◽  
Domain Theory ◽  
Invariance Property ◽  
Inverse Limits ◽  
Classical Domain ◽  
Contextual Equivalence

We develop an operational domain theory for treating recursive types with respect to contextual equivalence. The principal approach we take deviates from classical domain theory in that we do not produce the recursive types using the usual inverse limits constructions – we get them for free by working directly with the operational semantics. By extending type expressions to functors between some ‘syntactic’ categories, we establish algebraic compactness. To do this, we rely on an operational version of the minimal invariance property, for which we give a purely operational proof.

scholarly journals Denotational semantics of recursive types in synthetic guarded domain theory

2018 ◽  
Vol 29 (3) ◽  
pp. 465-510 ◽  
Author(s):  
RASMUS E. MØGELBERG ◽  
MARCO PAVIOTTI
Keyword(s):  
Programming Languages ◽  
Type Theory ◽  
Operational Semantics ◽  
Lambda Calculus ◽  
Denotational Semantics ◽  
Domain Theory ◽  
Logical Relation ◽  
Dependent Type Theory ◽  
Semantics Of Programming Languages ◽  
Dependent Type

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.

Sign in / Sign up

Export Citation Format

Share Document