Proper Treatment 正當作法/ Light seminar: Logic and computation
2013-11-20 16:26

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

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.

Calendar

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.