$B3'MM!"(B

$B0J2<$NFbMF$G#2#8F|!J7n!K$K9V1i$rFs7oM=Dj$7$F$$$^$9!#(B Herbelin$B$5$s$N9V1i$O(BFLOPS2012$B$N$*OC$N3HD%HG$G$9!#(B $B$I$&$>$4MhD0$/$@$5$$!#(B

$BD9C+@n???M(B [email protected] $B5~ETBg3X?tM}2r@O8&5f=j(B

====================================================

Date: 28 May 2012 (Monday) 14:30-17:00

14:30-15:30 talk by Vivek Nigam 16:00-17:00 talk by Hugo Herbelin

Venue: Room 478, General Research Building No.2, Kyoto University (Access information & map: http://www.kyoto-u.ac.jp/en/access http://www.kurims.kyoto-u.ac.jp/~hassei/map-2.jpg)

$BCm!'?tM}2r@O8&5f=jK\4[$G$O$"$j$^$;$s!#(B $BI4K|JW$N$=$P$NAm9g8&5fFs9f4[$N(B4$B3,$G$9!#(B

====================================================

Speaker: Vivek Nigam (Ludwig Maximilian University of Munich)

Title: An Extended Framework for Specifying and Reasoning about Proof Systems

Abstract: It has been shown that linear logic can be successfully used as a framework for both specifying proof systems for a number of logics, as well as proving fundamental properties about the specified systems. In this paper, we show how to extend the framework with subexponentials in order to be able to declaratively encode a wider range of proof systems, including a number of non-trivial proof systems such as a multi-conclusion intuitionistic logic, classical modal logic S4, and intuitionistic Lax logic. Moreover, we propose methods for checking whether an encoded proof system has important properties, such as if it admits cut-elimination, the completeness of atomic identity rules, and the invertibility of its inference rules. Finally, we present a tool implementing some of these specification/verification methods.

This is a joint work with Giselle Reis and Elaine Pimentel.

====================================================

Speaker: Hugo Herbelin (Laboratoire PPS, CNRS, INRIA & Universite Paris Diderot)

Title: Classical call-by-need sequent calculi: The unity of semantic artifacts

Abstract: We systematically derive a classical call-by-need sequent calculus, which does not require an unbounded search for the standard redex, by using the unity of semantic artifacts proposed by Danvy et al. The calculus serves as an intermediate step toward the generation of an environment-based abstract machine. The resulting abstract machine is context-free, so that each step is parametric in all but one component. The context-free machine elegantly leads to an environment-based CPS transformation. This transformation is observationally different from a natural classical extension of the transformation of Okasaki et al., due to duplication of un-evaluated bindings. We further demonstrate the usefulness of a systematic approach by deriving an abstract machine and CPS for an alternative classical call-by-need calculus.

(Joint work with Zena M. Ariola, Paul Downen, Keiko Nakata & Alexis Saurin)

====================================================