[Colloquium] Guest Speaker announcement

[Ponda Barnes]

Guest Speaker
 
Presented by: Toyota Technological Institute at Chicago
 
 
Speaker: James Cheney
Speaker's home page:  http://homepages.inf.ed.ac.uk/jcheney/
 
 
Date: Tuesday, April 17, 2007
Time: 10:00
Location: TTI-C Conference room
 
 
Title: Nominal logic programming
 
Abstract:
 
Syntactic proofs using structural induction principles are essential for
proving properties of formal systems (that is, metatheoretic reasoning).
Most formal languages encountered in computer science and mathematics, such
as programming languages, logics, and calculi for modeling concurrency and
security protocols, involve some form of names, name binding and scope.  In
informal exposition or reasoning, it is commonplace to resort to intuitive
"without loss of generality"
arguments concerning fresh names and renaming in order to reason at a high
level about such expressions without getting bogged down in trivial-seeming
details.
 
In completely formal proofs or implementations, it is not possible to ignore
these details; they must be addressed correctly.  While many approaches have
been considered for dealing with this problem (some, such as higher-order
abstract syntax, very successful), none combines the level of rigor we
expect of a formal proof with the level of flexibility we need to formalize
typical informal proofs "in the wild":
for example, no such approach provides rigorous, high-level support for
reasoning about generativity, as encountered in the semantics of references,
type inference algorithms such as Algorithm W, module systems, nonces in
security protocols, scope extrusion in concurrency calculi, and many other
situations.
 
In this talk, I will discuss recent work on using Gabbay and Pitts' nominal
abstract syntax approach and nominal logic, a first-order theory of names
and binding due Pitts, as the basis of a logic programming language in which
it is possible to define calculi using inference rules more-or-less as is
usually done on paper.  I will present a brief overview of the syntax and
semantics of nominal logic and of nominal logic programs, and then show how
to solve a specific technical obstacle that needs to be overcome in order to
be able to define and reason about calculi involving generativity.
 
If you have any questions or would like to meet the speaker, please contact
Ponda Barnes at pondabarnes at tti-c.org
For future TTI-C events, please go to http://ttic.uchicago.edu/cal/monrh.php
 
 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.cs.uchicago.edu/pipermail/colloquium/attachments/20070416/e61a9465/attachment-0001.htm