Alex Simpson: Research Papers



The papers are listed in chronological order, together with relevant bibliographic information. If you have problems downloading papers from this page then please contact me: Alex.Simpson@ed.ac.uk

Kripke Semantics for a Logical Framework.
Unpublished paper, presented at Workshop on Types for Proofs and Programs, Baastad, Sweden, June 1992.
Last revision July 1993.

Recursive types in Kleisli categories.
Unpublished paper, August 1992.
Last revision August 1992.

A characterisation of the least-fixed-point operator by dinaturality.
Revised version of paper in Theoretical Computer Science, 118:301-314, 1993.
Last revision September 1995.

The Proof Theory and Semantics of Intuitionistic Modal Logic.
PhD Thesis, December 1993, revised September 1994.
Last revision September 1994.
(postscript, pdf)

Reflection using the derivability conditions. With Seán Matthews.
Presented at International Conference in memory of Roberto Magari, Siena, Italy, April 1994.
In Logic and Algebra, A. Ursini and P. Agliano (editors), pp. 603-616, Marcel Dekker Inc, 1996.
Last revision August 1994.

Categorical completeness results for the simply-typed lambda-calculus.
In Typed Lambda Calculi and Applications, Proceedings TLCA '95, Springer LNCS 902, pp. 414-427, 1995.
Last revision December 1994.

Compositionality via cut-elimination: Hennessy-Milner logic for an arbitrary GSOS.
Tenth Annual IEEE Symposium on Logic in Computer Science, pp. 420-430, 1995.
Last revision March 1995.

The convex powerdomain in a category of posets realized by cpos.
In Category Theory and Computer Science, Proceedings CTCS '95, Springer LNCS 953, pp. 117-145, 1995.
Last revision May 1995.

A uniform approach to domain theory in realizability models. With John Longley.
Math. Struct. in Comp. Sci. 7:469-505, 1997.
Last revision September 1996.

Lazy Functional Algorithms for Exact Real Functionals.
In Mathematical Foundations of Computer Science 1998, Springer LNCS 1450, pp. 456-464, 1998.
Last revision May 1998.

Computational Adequacy in an Elementary Topos.
In Computer Science Logic, Proceedings CSL '98. Springer LNCS 1584, pp. 323-342, 1999.
Last revision January 1999.

Lambda Definability with Sums via Grothendieck Logical Relations. With Marcelo Fiore.
In Typed Lambda Calculi and Applications, Proceedings TLCA '99, Springer LNCS 1581, pp. 147-161, 1999.
Last revision January 1999.

Axioms and (Counter)examples in Synthetic Domain Theory. With Jaap van Oosten .
Annals of Pure and Applied Logic. 104:233-278, 2000.
Last Revision June 1999.

Elementary Axioms for Categories of Classes (Extended Abstract).
Fourteenth Annual IEEE Symposium on Logic in Computer Science, pp. 77-85, 1999.
Last revision April 1999. Ho hum ... I am still working on the full version, which I hope to finish soon.

The Largest Topological Subcategory of Countably-based Equilogical Spaces. With Matías Menni.
Proceedings of MFPS XV. Electronic Notes in Theoretical Computer Science, Vol. 20, 1999.
Last revision February 1999.

Equational Lifting Monads. With Anna Bucalo and Carsten Führmann .
Proceedings of CTCS '99. Electronic Notes in Theoretical Computer Science, Vol. 29, 1999.
Last revision August 1999.

Topological and Limit-space Subcategories of Countably-based Equilogical Spaces. With Matías Menni.
Math. Struct. in Comp. Sci., 12:739-770, 2002.
Extended journal version of MFPS XV paper. Last revision October 2001.

Complete Axioms for Categorical Fixed-point Operators. With Gordon Plotkin.
Fifteenth Annual IEEE Symposium on Logic in Computer Science, pp.30-41, 2000
Replaces the abstract: Properties of Fixed Points in Axiomatic Domain Theory, presented at Fixed-points in Computer Science, Brno, 1998.
Last revision April 2000.

An Equational Notion of Lifting Monad. With Anna Bucalo and Carsten Führmann .
Theoretical Computer Science, 294:31-60, 2003,
Journal version of CTCS 99 paper. Last revision December 2000.

A Universal Characterization of the Closed Euclidean Interval (Extended Abstract). With Martín Escardó.
Sixteenth Annual IEEE Symposium on Logic in Computer Science, pp.115-125, 2001
Last revision April 2001. Draft longer version, February 2001, comments welcome!

Verifying temporal properties using explicit approximants: completeness for context-free processes. With Ulrich Schöpp.
In Proceedings FOSSACS 2002, Springer LNCS 2303, pp. 372-386, 2002.
Last revision January 2002. Draft longer version, November 2001, comments welcome!

Comparing Functional Paradigms for Exact Real-number Computation. (Also in pdf ) With Andrej Bauer and Martín Escardó.
In Proceedings ICALP 2002, Springer LNCS 2380, pp. 488-500, 2002.
Last revision April 2002. Draft longer version, January 2002, comments welcome!

Computational Adequacy for Recursive Types in Models of Intuitionistic Set Theory (conference version, also in pdf )
Seventeenth Annual IEEE Symposium on Logic in Computer Science, pp. 287-298, 2002.
Last revision April 2002.

Computational Adequacy for Recursive Types in Models of Intuitionistic Set Theory (journal version, also in pdf)
Alex Simpson
In Annals of Pure and Applied Logic, 130:207-275, 2004.
(special issue for selected papers from LICS 02, ed. G. Plotkin)
Last revision December 2003.

Sequent Calculi for Process Verification: Hennessy-Milner Logic for an Arbitrary GSOS (also in pdf)
Alex Simpson
In Journal of Logic and Algebraic Programming, 60-61:287-322, 2004.
(special issue on structural operational semantics, eds. L. Aceto and W. Fokkink)
Last revision September 2003.
(Journal version of my LICS 95 paper.)

Towards a Convenient Category of Topological Domains
Alex Simpson
In Proceedings of thirteenth ALGI Workshop, RIMS, Kyoto University, 2003
Last revision April 2003.

Locally Non-compact Spaces and Continuity Principles (Also in pdf )
Andrej Bauer and Alex Simpson
In Proceedings of International Conference on Computability and Complexity in Analysis, Cincinatti, 2003
Fernuniversität Hagen Informatik Berichte 302 - 8/2003
Last revision July 2003.

Comparing Cartesian-closed Categories of (Core) Compactly Generated Spaces (Also in pdf )
Martín Escardó, Jimmie Lawson and Alex Simpson
In Topology and its Applications, 143:105-145, 2004.
Last revision February 2004.

Two Constructive Embedding-Extension Theorems with Applications to Continuity Principles and to Banach-Mazur Computability (Also in pdf )
Andrej Bauer and Alex Simpson
In Mathematical Logic Quarterly, 50:351-369, 2004.
(Journal version and extension of CCA 2003 paper.)
Last revision April 2004.

Using Synthetic Domain Theory to Prove Operational Properties of a Polymorphic Programming Language Based on Strictness (Also in pdf)
Giuseppe Rosolini and Alex Simpson
Manuscript. Last revision February 2004.

Constructive Set Theories and their Category-theoretic Models (Also in pdf)
Alex Simpson
In From Sets and Types to Topology and Analysis: Towards Practicable Foundations for Constructive Mathematics,
L. Crosilla and P. Schuster, eds., Oxford University Press, 2005.
Last revision October 2004.

Coalgebraic Semantics for Timed Processes (Also in pdf)
Marco Kick, John Power and Alex Simpson
Information and Computation, 204(4):588-609, 2006.
Special issue for selected papers from CMCS 2004
Last revision February 2005

Reduction in a Linear Lambda-calculus with Applications to Operational Semantics (Also in pdf)
Alex Simpson
In Proceedings RTA 2005
Nara, Japan, April 2005
Last revision February 2005

Representing Probability Measures using Probabilistic Processes (conference version)
Matthias Schröder and Alex Simpson
In Proceedings of Second International Conference on Computability and Complexity in Analysis
FernUniversität Hagen, Germany, Informatik Berichte, 326-7, 2005
(postscript, pdf)

Compactly Generated Domain Theory
Ingo Battenfeld, Matthias Schröder and Alex Simpson
Mathematical Structures in Computer Science, 16:141-161, 2006.
Special issue Festschrift for Klaus Keimel
M. Escardó, A. Jung and T. Streicher (eds)
(postscript, pdf)

Representing Probability Measures using Probabilistic Processes (journal version)
Matthias Schröder and Alex Simpson
Journal of Complexity, 22: 768--788, 2006
Special Issue on Computability, Complexity and Analysis
V. Brattka, P. Hertling, K-I. Ko and H. Tsuiki (eds)
(postscript, pdf)

Two Preservation Results for Countable Products of Sequential Spaces
Matthias Schröder and Alex Simpson
Mathematical Structures in Computer Science, 17(1):161-172, 2007
Special Issue on Constructive analysis, types and exact real numbers
H. Geuvers, M. Niqui, B. Spitters and F. Wiedijk (eds)
(postscript, pdf)

Probabilistic Observations and Valuations (Extended Abstract)
Matthias Schröder and Alex Simpson
In Proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXI)
Electronic Notes in Computer Science, 155: 605-615 , 2006
(postscript, pdf)

A Convenient Category of Domains
Ingo Battenfeld, Matthias Schröder and Alex Simpson
Computation, Meaning and Logic, Articles dedicated to Gordon Plotkin
L. Cardelli, M. Fiore and G. Winskel (eds)
Electronic Notes in Computer Science, 34 pp., to appear, 2007
(postscript, pdf)

Relating first-order set theories and elementary toposes
Steve Awodey, Carsten Butz, Alex Simpson and Thomas Streicher
Bulletin of Symbolic Logic. 13:340-358, 2007.
(postscript, pdf)

Two Probabilistic Powerdomains in Topological Domain Theory
Ingo Battenfeld and Alex Simpson
Manuscript December 2006
(postscript, pdf)

Relational Parametricity for Control Considered as a Computational Effect
Rasmus Møgelberg and Alex Simpson
Proceedings of Twenty-third Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXIII)
Electronic Notes in Computer Science 173:295-312, 2007
(postscript, pdf)

Relational Parametricity for Computational Effects
Rasmus Møgelberg and Alex Simpson
Proceedings of Twenty-second Annual IEEE Symposium on Logic in Computer Science, pp. 346-355, 2007.
(postscript, pdf)

Complete Sequent Calculi for Induction and Infinite Descent
James Brotherston and Alex Simpson
Proceedings of Twenty-second Annual IEEE Symposium on Logic in Computer Science, pp. 51-60, 2007.
(pdf)

A logic for parametric polymorphism with effects
Rasmus Møgelberg and Alex Simpson
In Types for Proofs and Programs (post-conference proceedings for selected papers from TYPES 2007)
Springer LNCS 4941, pp. 142-156, 2008.
Preprint (pdf)

Relational Parametricity for Computational Effects
Rasmus Møgelberg and Alex Simpson
Logical Methods in Computer Science, 5(3), 31 pp., 2009.
(Expanded journal version of LICS 2007 paper.)
Open access reprint (pdf)

Enriching an effect calculus with linear types
Jeff Egger, Rasmus Møgelberg and Alex Simpson
In Proceedings of Computer Science Logic 2009
Springer LNCS 5771, pp. 240-254, 2009.
Preprint (pdf)

Linearly-used continuations in the enriched effect calculus
Jeff Egger, Rasmus Møgelberg and Alex Simpson
In Proceedings FoSSaCS 2010
Springer LNCS 6014, pp. 18-32, 2010.
Preprint (pdf)

A generic operational metatheory for algebraic effects
Patricia Johann, Alex Simpson and Janis Voigtländer
Proceedings of Twenty-fifth Annual IEEE Symposium on Logic in Computer Science, pp. 209-218, 2010.
Preprint (pdf)

Sequent Calculi for Induction and Infinite Descent
James Brotherston and Alex Simpson
Journal of Logic and Computation, 21(6), pp. 1177-1216, 2011.
(Expanded journal version of LICS 2007 paper.)
Preprint (pdf)

Linear-use CPS translations in the enriched effect calculus
Jeff Egger, Rasmus Møgelberg and Alex Simpson
Logical Methods in Computer Science, 8(4), 27 pp., 2012.
(Expanded journal version of FOSSACS 2010 paper.)
Open access reprint (pdf)

Constructive toposes with countable sums as models of constructive set theory
Alex Simpson and Thomas Streicher
Annals of Pure and Applied Logic, 163(10), pp. 1419-1436, 2012.
Preprint (pdf)

Measure, Randomness and Sublocales
Alex Simpson
Annals of Pure and Applied Logic, 163(11), pp. 1642-1659, 2012.
Preprint (pdf)

The Enriched Effect Calculus: Syntax and Semantics
Jeff Egger, Rasmus Møgelberg and Alex Simpson
Journal of Logic and Computation, doi: 10.1093/logcom/exs025, published online: June 19, 2012.
(Expanded journal version of CSL 2009 paper.)
Preprint (pdf)

A Proof System for Compositional Verification of Probabilistic Concurrent Processes
Matteo Mio and Alex Simpson
In Proceedings FoSSaCS 2013
Lecture Notes in Computer Science Volume Springer LNCS 7794, pp. 161-176, 2013.
Preprint (pdf)

Relating first-order set theories, toposes and categories of classes
Steve Awodey, Carsten Butz, Alex Simpson and Thomas Streicher
Annals of Pure and Applied Logic, doi: 10.1016/j.apal.2013.06.004, published online: July 8, 2013.
Preprint (pdf)

Łukasiewicz μ-calculus
Matteo Mio and Alex Simpson
To appear in proceedings of Fixed-points in Computer Science (FICS) 2013, Turin, Italy, September 2013.
Preprint (pdf)