Spring 2007, Organizer: Chung-chieh Shan

Thursdays 5pm–6:20pm (note another time change)

The simple idea that programs are proofs has many uses. In particular, it helps

- design sophisticated data structures (such as algebraic data types) and control facilities (such as continuations and monads); and
- prove theorems such as the safety and correctness of a program or the security of a system.

We will examine these applications and their logical foundations, especially how they support interaction among distributed components. The goal is to approach open problems including the following.

- How safe can we ensure a program to be, using type systems practical today?
- How can we build and verify a system in which knowledge and services may be distributed and the external environment may be uncertain?
- What is a computational interpretation of classical modal logic? How does intuitionistic logic embed into it?
- What is a logical interpretation of delimited continuations? What duality does it expose?

## Calendar

- 1/18: Proofs are programs
- 1/25: (Adam Pantel) Typeful programming
- 2/1: (Jun Dai) Lambda-calculus schemata
- 2/8: continued
- 2/15: Probabilistic language
- 2/22: (Ken Shan) Constructor classes
- 2/26 at 3pm: continued
- 3/5 at 3pm: (John Austen) Network services
- 3/19 at 3pm: (Ken Shan) Symmetric modal
- 3/29: (Ken Shan) Distributed control
- 4/5: cancelled, sorry
- 4/12: Functional abstraction
- 4/19:
- 4/26:

## Logistics

The course number is 16:198:500:02. The index number is 48078.

The first meeting was in CoRE 305 from 3:20pm to 4:40pm on Thursday January 18. At this meeting, we introduced ourselves, settled administrative details, developed an initial schedule, and surveyed the topics to be covered.

Please send discussion to the email address logic-comp at rams dot rutgers dot edu.

Each student will “sponsor” one or more readings. We will cover about one reading per week, but some readings may take multiple weeks. The sponsor of each week’s reading will lead the discussion on the paper or a related example of programming or theorem proving. To help the sponsor prepare, all participants should email comments or questions to the list or the sponsor ahead of time. At the end of each meeting, the sponsor of the next week’s reading will spend five minutes to introduce it.

## Tentative reading list

The material listed below is clearly both too much (to cover in a single light seminar) and too little (to expose the variety of technical approaches). We will choose what to read by considering participant interests while respecting technical dependencies.

### Getting started

Mitzenmacher, Michael, and Norman Ramsey. 2001. How to read a research paper.

Wadler, Philip L. 2000. Proofs are programs: 19th century logic and 21st century computing.

Fischer, Michael J. 1993. Lambda-calculus
schemata. *Lisp and Symbolic Computation*
6(3–4):259–288.

Borghuis, Tijn, and Loe Feijs. 2000. A
constructive logic for services and information flow in computer
networks. *The Computer Journal* 43(4): 274–289.
(Download this article from within or
via Rutgers.)

### Programs of types

Cardelli, Luca. 1991. Typeful
programming. In *Formal description of programming
concepts*, ed. Erich J. Neuhold and Manfred Paul. Berlin:
Springer-Verlag.

Cardelli, Luca. 1997. Type systems.
In *The computer science and engineering handbook*, ed.
Allen B. Tucker, Jr., chap. 103, 2208–2236. Boca Raton, FL: CRC
Press.

Jones, Mark P. 1995. Functional
programming with overloading and higher-order polymorphism. In
*Advanced functional programming: 1st international spring
school on advanced functional programming techniques*, ed.
Johan Jeuring and Erik Meijer, 97–136. Lecture Notes in Computer
Science 925, Berlin: Springer-Verlag.

Kiselyov, Oleg, and Chung-chieh Shan. 2004. Functional
pearl: Implicit configurations—or, type classes reflect the value
of types. In *Proceedings of the 2004 Haskell workshop*,
33–44. New York: ACM Press.

Park, Sungwoo, Frank Pfenning, and Sebastian Thrun. 2006. A probabilistic language based upon sampling functions.

### Proofs of propositions

Appel, Andrew W. 2000. Hints on proving theorems in Twelf. (Two meetings?)

Bertot, Yves, and Pierre Castéran. 2004. *Interactive theorem
proving and program development: Coq’Art: The calculus of inductive
constructions*. EATCS Texts in Theoretical Computer Science,
Berlin: Springer-Verlag. (Two meetings?)

Halpern, Joseph Y. 1995.
Reasoning about knowledge: A survey. In *Handbook of logic
in artificial intelligence and logic programming. Volume 4:
Epistemic and temporal reasoning*, ed. Dov M. Gabbay,
Christopher John Hogger, and John Alan Robinson, 1–34. New York:
Oxford University Press.

Kiselyov, Oleg, and Chung-chieh Shan. 2006.
Lightweight static capabilities. In *PLPV 2006: Programming
languages meet program verification*, ed. Aaron Stump and
Hongwei Xi. Electronic Notes in Theoretical Computer Science,
Amsterdam: Elsevier Science.

Abadi, Martín. 2003. Logic in
access control. In *LICS 2003: Proceedings of the 18th
symposium on logic in computer science*, 228–233. Washington,
DC: IEEE Computer Society Press.

Abadi, Martín. 2006. Access
control in a core calculus of dependency. In *ICFP ‘06:
Proceedings of the ACM international conference on functional
programming*. New York: ACM Press.

### Undelimited continuations

Haynes, Christopher T., Daniel P. Friedman, and Mitchell Wand.
1986. Obtaining coroutines with continuations. *Computer
Languages* 11(3–4): 143–153.

Ong, C.-H. Luke. 1996.
A semantic view of classical proofs: Type-theoretic, categorical,
and denotational characterizations. In *LICS ‘96:
Proceedings of the 11th symposium on logic in computer
science*, 230–241. Washington, DC: IEEE Computer Society
Press.

Ong, C.-H. Luke, and Charles Alexander Stewart. 1997.
A Curry-Howard foundation for functional computation with
control. In *POPL ‘97: Conference record of the annual ACM
symposium on principles of programming languages*, 215–227.
New York: ACM Press.

Wadler, Philip L. 2003. Call-by-value
is dual to call-by-name. In *ICFP ‘03: Proceedings of the
ACM international conference on functional programming*, vol.
38(9) of *ACM SIGPLAN Notices*. New York: ACM Press.

Murphy, Tom, VII, Karl Crary, and Robert Harper. 2005. Distributed
control flow with classical modal logic. In *Computer
science logic: 19th international workshop, CSL 2005*, ed.
C.-H. Luke Ong, 51–69. Lecture Notes in Computer Science 3634,
Berlin: Springer-Verlag.

### Delimited continuations

Biernacki, Dariusz, Olivier Danvy, and Chung-chieh Shan. 2006.
On the
static and dynamic extents of delimited continuations.
*Science of Computer Programming* 60(3):274–297.

Danvy, Olivier, and Andrzej Filinski. 1989. A functional abstraction of typed contexts. Tech. Rep. 89/12, DIKU, University of Copenhagen, Denmark.

Barker, Chris, and Chung-chieh Shan. 2006. Types as
graphs: Continuations in type logical grammar. *Journal of
Logic, Language and Information* 15(4): 331–370.