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)