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.
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
To appear in From Sets and Types to Topology and Analysis:
Towards Practicable Foundations
for Constructive Mathematics,
L. Crosilla and P. Schuster, eds.,
Oxford University Press, forthcoming.
Last revision October 2004.
Coalgebraic Semantics for Timed Processes
(Also in pdf)
Marco Kick, John Power and Alex Simpson
To appear in Information and Computation,
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, vol. 17, No. 1, 12pp.,
to appear 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
Submitted November 2006.
(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
A revised version will appear in
Proceedings LICS 2007
(postscript,
pdf)
A logic for parametric polymorphism with effects
Rasmus Møgelberg and Alex Simpson
To appear in post-conference proceedings for selected papers from TYPES 2007
Springer LNCS, to appear 2008.
(postscript,
pdf)
Enriching an effect calculus with linear types
Jeff Egger, Rasmus Møgelberg and Alex Simpson
To appear in proceedings of Computer Science Logic 2009
Springer LNCS, 2009.
(pdf)
A generic operational metatheory for algebraic effects
Patricia Johann, Alex Simpson and Janis Voigtländer
Submitted, October 2009.
(pdf)