Relational Parametricity for Computational Effects (2009)
Møgelberg, Rasmus Ejlers, Simpson, Alex
According to Strachey, a polymorphic program is parametric if it applies a uniform algorithm independently of the type instantiations at which it is applied. The notion of relational parametricity,...
Relational parametricity for control considered as a computational effect (2009)
Rasmus Ejlers Møgelberg, Alex Simpson
Replace this file with prentcsmacro.sty for your meeting, or with entcsmacro.sty for your meeting. Both can be
Denotational semantics seeks to provide compositional models of computation, programs and data at the right level of abstraction to be independent of language-specific and implementation details, and...
Anna Bucalo, Alex Simpson, Carsten Führmann
We introduce the notion of an equational lifting monad: a commutative strong monad satisfying one additional equation (valid for monads arising from partial map classifiers). We prove that any...
A logic for parametric polymorphism with effects (2008)
Rasmus Ejlers Møgelberg, Alex Simpson
Abstract. We present a logic for reasoning about parametric polymorphism in combination with arbitrary computational effects (nondeterminism, exceptions, continuations, side-effects etc.). As...
Polymorphism is a feature of many programming languages, including typed functional languages (e.g., SML, Haskell), and recent “generic ” versions of Java. Relational parametricity, introduced by...
Relational parametricity for control considered as a computational effect (2008)
Rasmus Ejlers Møgelberg, Alex Simpson
Replace this file with prentcsmacro.sty for your meeting, or with entcsmacro.sty for your meeting. Both can be
Ingo Battenfeld, Matthias Schröder, Alex Simpson
We propose compactly generated monotone convergence spaces as a well-behaved
We prove two embedding and extension theorems in the context of the constructive theory of metric spaces. The first states that Cantor space embeds in any inhabited complete separable metric space...
We prove two embedding and extension theorems in the context of the constructive theory of metric spaces. The first states that Cantor space embeds in any inhabited complete separable metric space...
Sequent Calculi for Process Verification: Hennessy-Milner Logic for an Arbitrary GSOS (2008)
We argue that, by supporting a mixture of "compositional" and "structural" styles of proof, sequent-based proof systems provide a useful framework for the formal verification of...
There are two main approaches to obtaining "topological " cartesian-closed categories. Under one approach, one restricts to a full subcategory of topological spaces that happens to...
Beyond Classical Domain Theory 5/75 (2007)
domain = pointed dcpo morphism = continuous function • Every endomorphism f: D → D has least fixed point. (Models recursion) • Nontrivial solutions to D ∼ = D D. (Models untyped λ-calculus)...
A convenient category of domains (2007)
Battenfeld, Ingo, Schröder, Matthias, Simpson, Alex
We motivate and define a category of "topological domains", whose objects are certain topological spaces, generalising the usual $omega$-continuous dcppos of domain theory. Our category supports all...
Complete sequent calculi for induction and infinite descent (2007)
James Brotherston, Alex Simpson
Abstract. This paper formalises and compares two different styles of reasoning with inductively defined predicates, each style being encapsulated by a corresponding sequent calculus proof system. The...
Coalgebraic semantics for timed processes (2006)
Marco Kick, John Power, Alex Simpson
We give a coalgebraic formulation of timed processes and their operational semantics. We model time by a monoid called a “time domain”, and we model processes by “timed transition systems”,...
Andrews, Gordon E., Zhu, G., Li, Hu, Simpson, Alex, Wylie, James A., Bell, Margaret, ...
The influence of ambient temperature on exhaust emissions for an instrumented Euro 1 SI car was determined. A real world test cycle was used, based on an urban drive cycle that was similar to the ECE...
Reduction in a linear lambda-calculus with applications to operational semantics (2005)
Abstract. We study beta-reduction in a linear lambda-calculus derived from Abramsky’s linear combinatory algebras. Reductions are classified depending on whether the redex is in the computationally...
Comparing cartesian closed categories of (2004)
Martín Escardó, Jimmie Lawson, Alex Simpson, Martín Escardó, Jimmie Lawson, Alex Simpson
(core) compactly generated spaces
We prove two embedding and extension theorems in the context of the constructive theory of metric spaces. The first states that Cantor space embeds in any inhabited complete separable metric space...
An equational notion of lifting monad (2003)
Anna Bucalo, Carsten Fuhrmann, Alex Simpson
We introduce the notion of an equational lifting monad: a commutative strong monad satisfying one additional equation (valid for monads arising from partial map classifiers). We prove that any...
An Equational Notion of Lifting Monad (2003)
Anna Bucalo, Carsten Führmann, Alex Simpson
We introduce the notion of an equational lifting monad: a commutative strong monad satisfying one additional equation (valid for monads arising from partial map classifiers). We prove that any...
Locally Non-compact Spaces and Continuity Principles (2003)
We give a constructive proof that Baire space embeds in any inhabited locally non-compact complete separable metric space, X, in such a way that every sequentially continuous function from Baire...
We prove two embedding and extension theorems in the context of the constructive theory of metric spaces. The first states that Cantor space embeds in any inhabited complete separable metric space...
Sequent Calculi for Process Verification: Hennessy-Milner Logic for an Arbitrary GSOS (2003)
We argue that, by supporting a mixture of “compositional” and “structural” styles of proof, sequent-based proof systems provide a useful framework for the formal verification of processes. As...
Comparing functional paradigms for exact real-number computation (2002)
Andrej Bauer, Martín Hötzel Escardó, Alex Simpson
Abstract. We compare the definability of total functionals over the reals in two functional-programming approaches to exact real-number datatype of real numbers; and the intensional approach, in...
Comparing functional paradigms for exact real-number computation (2002)
Andrej Bauer, Martín Hötzel Escardó, Alex Simpson
Abstract. We compare the definability of total functionals over the reals in two functional-programming approaches to exact real-number datatype of real numbers; and the intensional approach, in...
Computational Adequacy for Recursive Types in Models of Intuitionistic Set Theory (2002)
We present a general axiomatic construction of models of FPC, a recursively typed lambda-calculus with call-byvalue operational semantics. Our method of construction is to obtain such models as full...
We present a sequent calculus for formally verifying modal-calculus properties of concurrent processes. Building on work by Dam and Gurov, the proof system contains rules for the explicit...
Abstract. We present a sequent calculus for formally verifying modal-calculus properties of concurrent processes. Building on work by Dam and Gurov, the proof system contains rules for the explicit...
Abstract. We present a sequent calculus for formally verifying modal-calculus properties of concurrent processes. Building on work by Dam and Gurov, the proof system contains rules for the explicit...
Comparing functional paradigms for exact real-number computation (2002)
Andrej Bauer, Martn Hotzel Escardo, Alex Simpson
Abstract. We compare the definability of total functionals over the reals in two functional-programming approaches to exact real-number datatype of real numbers; and the intensional approach, in...
Computational Adequacy for Recursive Types in Models of Intuitionistic Set Theory (2002)
This paper provides a unifying axiomatic account of the interpretation of recursive types that incorporates both domain-theoretic and realizability models as concrete instances. Our approach is to...
Abstract. We present a sequent calculus for formally verifying modal µ-calculus properties of concurrent processes. Building on work by Dam and Gurov, the proof system contains rules for the...
Computational Adequacy for Recursive Types in Models of Intuitionistic Set Theory (2002)
This paper provides a unifying axiomatic account of the interpretation of recursive types that incorporates both domain-theoretic and realizability models as concrete instances. Our approach is to...
Complete Axioms for Categorical Fixed-point Operators (2000)
We give an axiomatic treatment of fixed-point operators in categories. A notion of iteration operator is defined, embodying the equational properties of iteration theories. We prove a general...
Complete axioms for categorical fixed-point operators (2000)
We give an axiomatic treatment of fixed-point operators in categories. A notion of iteration operator is defined, embodying the equational properties of iteration theories. We prove a general...
Equational lifting monads (1999)
Anna Bucalo, Carsten Führmann, Alex Simpson
We introduce the notion of an equational lifting monad: a commutative strong monad satisfying one additional equation (valid for monads arising from partial map classifiers). We prove that any...
There are two main approaches to obtaining “topological ” cartesian-closed categories. Under one approach, one restricts to a full subcategory of topological spaces that happens to be cartesian...
Topological and Limit-space subcategories of Countably-based Equilogical Spaces (1999)
this paper we show that the two approaches are equivalent for a
Lambda Definability with Sums via Grothendieck Logical Relations (1999)
. We introduce a notion of Grothendieck logical relation and use it to characterise the definability of morphisms in stable bicartesian closed categories by terms of the simply-typed lambda calculus...
Equational Lifting Monads (1999)
Anna Bucalo, Carsten Führmann, Alex Simpson
We introduce the notion of an equational lifting monad: a commutative strong monad satisfying one additional equation (valid for monads arising from partial map classifiers). We prove that any...
Lambda Definability with Sums via Grothendieck Logical Relations (1999)
. We introduce a notion of Grothendieck logical relation and use it to characterise the definability of morphisms in stable bicartesian closed categories by terms of the simply-typed lambda calculus...
The Largest Topological Subcategory of Countably-based Equilogical Spaces (1998)
There are two main approaches to obtaining "topological" cartesian-closed categories. Under one approach, one restricts to a full subcategory of topological spaces that happens to be...