Penn Logic and Computation Seminar 1998-1999

The logic and computation group is composed of faculty and graduate students from the computer and information science, mathematics, and philosophy departments, and participates in the Institute for Research in the Cognitive Sciences.

The logic and computation group runs a weekly seminar. The seminar meets regularly during the school year on Mondays at 4:30 p.m. in room 4C8 of the David Rittenhouse Laboratory at the University of Pennsylvania. Any changes to this schedule will be specifically noted. The seminar is open to the public and all are welcome. Directions to DRL can be found here.

Upcoming/recent Talks

May 13: Tommy Thorn, IRISA Verification of control flow based security properties
Apr 29: Roberto Di Cosmo, Ecole Normale Superieure, Paris Parallel functional programming: the OcamlP3l experiment
Apr 16: Robert Harper, CMU What is a Recursive Module?
Mar 15: Anthony Bonner, U. Toronto and U. Penn Workflow, Transactions, and Logic
Mar 1: Hongde Hu, U. Penn Contractible graphs and fair games
Feb 8: Max Kanovitch (Russian State University for the Humanities, Moscow, and U. Penn) The Undecidability of Propositional Linear Logic Without Variables

Linear logic was introduced by Girard as a resource-sensitive refinement of classical logic. It turned out that full propositional linear logic is undecidable (Lincoln, Mitchell, Scedrov, and Shankar) and, hence, it is more expressive than (modalized) classical or intuitionistic logic. Here we focus on the study of the simplest fragments of linear logic, such as the one-variable and constant-only fragments (the latter contains no variables at all).

Here we prove that all these extremely simple fragments of linear logic (one-variable, bottom-only, and even unit-only) are exactly of the same expressive power as the corresponding full versions with an unbounded number of variables. In particular, 1. On the level of multiplicatives only we get NP-completeness. 2. Enriching this basic set of connectives by additives yields PSPACE-completeness. 3. Using in addition the modal operator !, we can prove undecidability of each of these three fragments.

Previous Talks

September 23, IRCS [note nonstandard day / place]: Masako Takahashi (Tokyo Institute of Technology), Parallel Reductions in Lambda-Calculus
September 24, IRCS [note nonstandard day / place]: Masako Takahashi (Tokyo Institute of Technology), Lambda-Representable Functions over Free Structures
Oct. 19: Natasha Kurtonina (U. Penn), Modal logics lacking booleans: bisimulations and model theoretic behavior
Nov. 2: Philip Wadler (Lucent), GJ: Making Java easier to type, and easier to type
Nov. 9: Kim Bruce (Williams College), Modules in LOOM: Classes are not enough
Nov. 16: Anatol Holt, Universita di Milano Some Computer-Related Conundrums
Nov. 30: Radu Grosu, University of Pennsylvania (and TU Muenchen) Towards a Formal Foundation for UML-RT
Jan. 18: Atsushi Igarashi, University of Pennsylvania (and U. Tokyo) Foundations for Virtual Types
Feb 1: Uwe Nestmann, BRICS Migration = Cloning ; Aliasing

Seminars from previous years