Publications

Thesis proposal

Kevin Watkins, "CLF: A logical framework for concurrent systems," Thesis proposal, Department of Computer Science, Carnegie Mellon University, May 2003.

Slides from the thesis proposal talk.

Refereed conference papers

Pablo López, Frank Pfenning, Jeff Polakow, and Kevin Watkins, "Monadic Concurrent Linear Logic Programming," 7th International Symposium on Principles and Practice of Declarative Programming (PPDP '05), July 2005, Lisbon, Portugal. Draft of February 2005. To appear.

David Walker and Kevin Watkins, "On Regions and Linear Types," Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming (ICFP '01), September 3-5, 2001, Florence, Italy, pp. 181-192.

Joshua S. Hodas, Kevin Watkins, Naoyuki Tamura, and Kyoung-Sun Kang, "Efficient Implementation of a Linear Logic Programming Language," Proceedings of the 1998 Joint International Conference and Symposium on Logic Programming, June 15-19, 1998, Manchester, U.K., pp. 145-159.

R. Libeskind-Hadas, T. Hehre, A. Hutchings, M. Reyes, and K. Watkins, "Adaptive Multicast Routing in Wormhole Networks," Proceedings of the Ninth IASTED International Conference on Parallel and Distributed Computing and Systems, October 13-16, 1997, Washington, D.C., pp. 513-522.

R. Libeskind-Hadas, K. Watkins, and T. Hehre, "Fault-Tolerant Multicast Routing in the Mesh with No Virtual Channels," Proceedings of the 1996 International Symposium on High-Performance Computer Architecture (HPCA '96), February 3-7, 1996, San Jose, California, pp. 180-190.

Workshops

Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker, "Specifying properties of concurrent computations in CLF," In C. Schürmann, editor, Proceedings of the 4th International Workshop on Logical Frameworks and Meta-Languages (LFM '04), July 2004, Cork, Ireland.

Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker, "A concurrent logical framework: The propositional fragment," In S. Berardi, M. Coppo, and F. Damiani, editors, Types for Proofs and Programs, pp. 355-377. Springer-Verlag LNCS 3085, 2004. Revised selected papers from the Third International Workshop on Types for Proofs and Programs, April 2003, Torino, Italy.

David Walker and Kevin Watkins, "On Regions and Linear Types," at the Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management, January 2001, London, UK. A revised version of this work appeared at ICFP'01.

Technical reports

Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker, "A concurrent logical framework I: Judgments and properties," Technical Report CMU-CS-02-101, Department of Computer Science, Carnegie Mellon University, March 2002, revised May 2003.

Iliano Cervesato, Frank Pfenning, David Walker, and Kevin Watkins, "A concurrent logical framework II: Examples and applications," Technical Report CMU-CS-02-102, Department of Computer Science, Carnegie Mellon University, March 2002, revised May 2003.

R. Libeskind-Hadas, K. Watkins, and T. Hehre, "Fault-tolerant multicast routing in the mesh with no virtual channels," Technical Report HMC-CS-95-03, Harvey Mudd College, Department of Computer Science, June 1995.

Seminar talks

"Abstract Interpretation Using Laziness: Proving Conway's Lost Cosmological Theorem," POP seminar talk, Carnegie Mellon University, December 2006. Slides from the talk.

"Defining an operational semantics for resource management in Lolli", Dagstuhl Seminar 01141 on Semantic Foundations of Proof-search, April 2-6, 2001, Wadern, Germany.

Manuscripts

Kevin Watkins, "Abstract Interpretation Using Laziness: Proving Conway's Lost Cosmological Theorem," Writing Skills paper, December 2006. Not yet submitted for publication.

Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker, "A Dependent Logical Framework for Concurrent Computations." Unpublished manuscript, July 2004.

Dominic Mazzoni and Kevin Watkins, Uncrossed Knight Paths is NP-complete, 1997. This is related to the complexity of the game Twixt.

Drafts

[CMU only]

These are often extremely fragmentary accounts of work in progress, and are almost certain to contain highly bogus material. Caveat lector. These drafts are not to be circulated or redistributed in any form without my prior permission.

A module system for LF. A simple module system that can be elaborated away into pure core LF constructs. [dvi]

Syntactic redundancy for LF. The idea being to annotate an LF signature for information flow during term reconstruction so that reconstruction becomes decidable and efficient. [dvi]

Resource management for Lolli. A fixed-up operational semantics for Lolli using tags. This has been superseded by other work (Lopez and Pimentel LPAR99). [dvi]

Also, a characterization (not supplied by any of the existing accounts of resource management for Lolli) of just what a resource management system should do, operationally. [dvi]

Courses

Some scribed notes from the Spring 2000 course on Typed Compilation:

The LaTeX source relies on a set of macros I've cobbled together over the years.