Lars Birkedal's Public Papers and Software

Logics of Types and Computation / Categorical Logic and Type Theory

confdt.ps.gz: Continuous Functionals of Dependent Types and Equilogical Spaces. Andrej Bauer and Lars Birkedal. Submitted for publication. January 2000.
locrtm.ps.gz: Local Realizability Toposes and a Modal Logic for Computability. Steven Awodey, Lars Birkedal, and Dana S. Scott. Submitted for publication. January 2000.
gennr.ps.gz gennr.ps: A General Notion of Realizability. Lars Birkedal. December 1999. Submitted for publication.
elealm.ps.gz: Elementary Axioms for Local Maps of Toposes. Steven Awodey and Lars Birkedal. November 1999. Technical Report No. CMU-PHIL103. Submitted for publication.
lrtmlc.ps.gz: Local Realizability Toposes and a Modal Logic for Computability. Steven Awodey, Lars Birkedal, Dana Scott. April, 1999. To Appear In Proceedings of Workshop on Realizability Semantics and its Applications, Trento, Italy, 1999.
equ.ps.gz: Equilogical Spaces.Andrej Bauer, Lars Birkedal, Dana Scott. September, 1998. Submitted for publication.
typtec.ps.gz: Type Theory via Exact Categories. Lars Birkedal, Aurelio Carboni, Guiseppe Rosolini, and Dana S. Scott. In Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science (LICS 1998).

Operational Semantics

conirt.ps.gz

Constructing Interpretations of Recursive Types in an Operational Setting. Lars Birkedal and Robert Harper. To Appear in Information and Computation.

tacs97.ps.gz

Constructing Interpretations of Recursive Types in an Operational Setting (Summary). Lars Birkedal and Robert Harper. TACS 1997. Superseded by conirt.ps.gz

opreln-tr.ps.gz

Constructing Interpretations of Recursive Types in an Operational Setting. Lars Birkedal and Robert Harper. Technical Report CMU-CS-98-125. April 1998. Superseded by conirt.ps.gz

Region Inference

conria.ps.gz: A Constraint-based Region Inference Algorithm. Lars Birkedal and Mads Tofte. To Appear in Theoretical Computer Science.
milner.ps.gz: Unification and Polymorphism in Region Inference. Mads Tofte and Lars Birkedal. To Appear in Milner Festschrift.
reginfalgo.ps.gz: A Region Inference Algorithm. Mads Tofte and Lars Birkedal. ACM Transactions on Programming Languages and Systems, Vol. 20, No. 5, July 1998. Pages 724-767 (+ appendix pages 1-26).
rri-popl96.ps.gz: From Region Inference to von Neumann Machines via Region Representation Inference. Lars Birkedal and Mads Tofte and Magnus Vejlstrup. 23rd ACM Symposium on Principles of Programming Languages. January 1996.

Partial Evaluation

smlmix.ps.gz: Partial Evaluation of Standard ML. Lars Birkedal and Morten Welinder. September 1993. Technical Report 93/22, DIKU, University of Copenhagen, Master's Thesis.
smlbta.ps.gz: Binding-Time Analysis for Standard ML. Lars Birkedal and Morten Welinder. June 1994. PEPM-94.
smlbta-lasc.ps.gz: Binding-Time Analysis for Standard ML. Lars Birkedal and Morten Welinder. Lisp and Symbolic Computation, Volume 8, Number 3, September 1995.
handcogen.ps.gz: Handwriting Program Generator Generators. Lars Birkedal and Morten Welinder. September 1994. PLILP-94.
SML-Mix: Home Page for SML-Mix.

The ML Kit

The ML Kit Project: The ML Kit Project Home Page.
manual.ps.gz: Programming with Regions in the ML Kit (for Version 3). Mads Tofte, Lars Birkedal, Martin Elsman, Niels Hallenberg, Tommy Hoejfeld Olesen, Peter Sestoft, Peter Bertelsen. Technical Report 98/25, DIKU, University of Copenhagen.
diku97-12.a4.ps.gz (A4 paper) or diku97-12.letter.ps.gz (US letter paper): Programming with Regions in the ML Kit. Mads Tofte, Lars Birkedal, Martin Elsman, Niels Hallenberg, Tommy Hoejfeld Olesen, Peter Sestoft, Peter Bertelsen. Technical Report 97/12, DIKU, University of Copenhagen.
kit.ps.gz: The ML Kit, Version 1. Lars Birkedal, Nick Rothwell, Mads Tofte, and David N. Turner. 1993. Technical Report 93/14, DIKU, University of Copenhagen.
kit.tar.gz: The ML Kit, Version 1. Lars Birkedal, Nick Rothwell, Mads Tofte, and David N. Turner. 1993. The tar file contains the sources and the documentation for The ML Kit (i.e. it includes the kit.ps.gz). Unpack the tar file and read the README file for directions.

Higher-Order Modules for Standard ML

hof.ps.gz: Higher-Order Functors and Principal Signatures in Standard ML. Lars Birkedal. September 1993. TOPPS Report D-184, DIKU, University of Copenhagen.

FTP Instructions

To retrieve files by anonymous FTP, proceed as follows. Remember to set the connection type to binary; otherwise compressed files will come out as garbage on the other end!

    ftp ftp.cs.cmu.edu             [or 128.2.206.173]
    login: anonymous
    password:
    cd /afs/cs/user/birkedal/pub
    binary                         [don't forget this!]
    get <name>.dvi.gz              [or <name>.ps.gz, etc.]

Please let me know if you have trouble printing anything.

Enjoy,

Lars Birkedal