Logics of Types and Computation at CMU

Welcome to the home page of the Logics of Types and Computation group at CMU, led by Prof. Dana S. Scott.

A description of our work.

Our recent activities

We edited a Bibliography on Realizability
We helped organize the Tutorial Workshop on Realizability Semantics and Applications in Trento, Italy, 1999.

People

A Selection of Papers

(Reverse chronological order)

S. Awodey, J. Hughes. Modal Operators for Coequations.
August 2001.: [Abstract] [gzip postscript]
A. Bauer, D.S. Scott. A New Category for Semantics.
June 2001. Notes from D.S. Scott's talk at MFCS 2001.: [Abstract] [postscript]
S. Awodey, A. Bauer. Propositions as [Types].
April 2001. Technical report at Insitut Mittag-Leffler.: [Abstract] [postscript] [gzip postscript] [postscript A4] [gzip postscript A4] [PDF] [PDF A4]
S. Awodey, A. Bauer. Sheaf Toposes for Realizability.
April 2001. Technical report CMU-PHIL-117.: [Abstract] [postscript] [gzip postscript] [postscript A4] [gzip postscript A4] [PDF]
A. Bauer, L. Birkedal, D.S. Scott. Equilogical Spaces.
September 1998. Revised February 2001. To appear in Theoretical Computer Science.: [Abstract] [postscript] [gzip postscript] [PDF]
A. Bauer The Realizability Approach to Computable Analysis and Topology.
Ph.D. Thesis. September 2000.: [Abstract & Further Information] [postscript] [gzip postscript] [PDF]
S. Awodey, J. Hughes. The Coalgebraic Dual of Birkhoff's Variety Theorem.
October 2000. Preprint.: [gzip postscript]
L. Birkedal, J. van Oosten. Relative and Modified Relative Realizability.
March 2000. Preprint 1146, Department of Mathematics, Universiteit Utrecht.: [gzip postscript]
A. Bauer, L. Birkedal. Continuous Functionals of Dependent Types and Equilogical Spaces.
January 2000. Proceedings of Computer Science Logic Conference 2000.: [gzip postscript] [PDF]
S. Awodey, L. Birkedal, D.S. Scott. Local Realizability Toposes and a Modal Logic for Computability.
January 2000. To apear in Math. Struct. in Comp. Sci.: [Abstract] [gzip postscript]
L. Birkedal. A General Notion of Realizability.
December 1999. Proceedings of LICS 2000: [Abstract] [gzip postscript]
L. Birkedal. Developing Theories of Types and Computability via Realizability.
PhD-thesis. December 1999. Electronic Notes in Theoretical Computer Science, 34, 2000.
Available at http://www.elsevier.nl/locate/entcs/volume34.html.: [Abstract] [gzip postscript] [PDF with active URLs]
S. Awodey and L. Birkedal. Elementary Axioms for Local Maps of Toposes.
November 1999. Technical Report No. CMU-PHIL-103. To appear in Journal of Pure and Applied Algebra.: [Abstract] [gzip postscript]
S. Awodey. Topological Representation of the Lambda Calculus.
September 1998. Math. Struct. in Comp. Sci. (2000), vol. 10, pp. 81--96.: [Abstract] [gzip postscript]
L. Birkedal, A. Carboni, G. Rosolini, and D.S. Scott. Type Theory via Exact Categories.
July 1998. Proceedings of LICS 1998.: [Abstract] [gzip postscript]
D.S. Scott. A New Category? Domains, Spaces and Equivalence Relations.
Manuscript. December 1996.: [Abstract] [postscript] [gzip postscript] [gzip postscript A4]