[logic-ml] talks by Vivek Nigam and Hugo Herbelin in Kyoto (28th May 2012)

[Hasegawa Masahito]

$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+ at n???M(B <hassei at kurims.kyoto-u.ac.jp>
$B5~ETBg3X?tM}2r at 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 at 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)

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