<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:st1="urn:schemas-microsoft-com:office:smarttags" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv=Content-Type content="text/html; charset=us-ascii">
<meta name=ProgId content=Word.Document>
<meta name=Generator content="Microsoft Word 11">
<meta name=Originator content="Microsoft Word 11">
<link rel=File-List href="cid:filelist.xml@01C780C8.A9506020">
<o:SmartTagType namespaceuri="urn:schemas-microsoft-com:office:smarttags"
name="City"/>
<o:SmartTagType namespaceuri="urn:schemas-microsoft-com:office:smarttags"
name="place"/>
<!--[if gte mso 9]><xml>
<o:OfficeDocumentSettings>
<o:DoNotRelyOnCSS/>
</o:OfficeDocumentSettings>
</xml><![endif]--><!--[if gte mso 9]><xml>
<w:WordDocument>
<w:SpellingState>Clean</w:SpellingState>
<w:DocumentKind>DocumentEmail</w:DocumentKind>
<w:EnvelopeVis/>
<w:ValidateAgainstSchemas/>
<w:SaveIfXMLInvalid>false</w:SaveIfXMLInvalid>
<w:IgnoreMixedContent>false</w:IgnoreMixedContent>
<w:AlwaysShowPlaceholderText>false</w:AlwaysShowPlaceholderText>
<w:Compatibility>
<w:BreakWrappedTables/>
<w:SnapToGridInCell/>
<w:WrapTextWithPunct/>
<w:UseAsianBreakRules/>
<w:UseWord2002TableStyleRules/>
<w:UseFELayout/>
</w:Compatibility>
<w:BrowserLevel>MicrosoftInternetExplorer4</w:BrowserLevel>
</w:WordDocument>
</xml><![endif]--><!--[if gte mso 9]><xml>
<w:LatentStyles DefLockedState="false" LatentStyleCount="156">
</w:LatentStyles>
</xml><![endif]--><!--[if !mso]>
<style>
st1\:*{behavior:url(#default#ieooui) }
</style>
<![endif]-->
<style>
<!--
/* Font Definitions */
@font-face
{font-family:SimSun;
panose-1:2 1 6 0 3 1 1 1 1 1;
mso-font-alt:\5B8B\4F53;
mso-font-charset:134;
mso-generic-font-family:auto;
mso-font-pitch:variable;
mso-font-signature:3 135135232 16 0 262145 0;}
@font-face
{font-family:"\@SimSun";
panose-1:2 1 6 0 3 1 1 1 1 1;
mso-font-charset:134;
mso-generic-font-family:auto;
mso-font-pitch:variable;
mso-font-signature:3 135135232 16 0 262145 0;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{mso-style-parent:"";
margin:0pt;
margin-bottom:.0001pt;
mso-pagination:widow-orphan;
font-size:12.0pt;
font-family:"Times New Roman";
mso-fareast-font-family:SimSun;
mso-fareast-language:ZH-CN;}
a:link, span.MsoHyperlink
{color:blue;
text-decoration:underline;
text-underline:single;}
a:visited, span.MsoHyperlinkFollowed
{color:purple;
text-decoration:underline;
text-underline:single;}
p.MsoAutoSig, li.MsoAutoSig, div.MsoAutoSig
{margin:0pt;
margin-bottom:.0001pt;
mso-pagination:widow-orphan;
font-size:12.0pt;
font-family:"Times New Roman";
mso-fareast-font-family:"Times New Roman";}
pre
{margin:0pt;
margin-bottom:.0001pt;
mso-pagination:widow-orphan;
font-size:10.0pt;
font-family:"Courier New";
mso-fareast-font-family:SimSun;}
span.EmailStyle19
{mso-style-type:personal;
mso-style-noshow:yes;
mso-ansi-font-size:10.0pt;
mso-bidi-font-size:10.0pt;
font-family:Arial;
mso-ascii-font-family:Arial;
mso-hansi-font-family:Arial;
mso-bidi-font-family:Arial;
color:windowtext;}
span.EmailStyle20
{mso-style-type:personal-reply;
mso-style-noshow:yes;
mso-ansi-font-size:10.0pt;
mso-bidi-font-size:10.0pt;
font-family:Arial;
mso-ascii-font-family:Arial;
mso-hansi-font-family:Arial;
mso-bidi-font-family:Arial;
color:navy;}
@page Section1
{size:612.0pt 792.0pt;
margin:72.0pt 90.0pt 72.0pt 90.0pt;
mso-header-margin:36.0pt;
mso-footer-margin:36.0pt;
mso-paper-source:0;}
div.Section1
{page:Section1;}
-->
</style>
<!--[if gte mso 10]>
<style>
/* Style Definitions */
table.MsoNormalTable
{mso-style-name:"Table Normal";
mso-tstyle-rowband-size:0;
mso-tstyle-colband-size:0;
mso-style-noshow:yes;
mso-style-parent:"";
mso-padding-alt:0pt 5.4pt 0pt 5.4pt;
mso-para-margin:0pt;
mso-para-margin-bottom:.0001pt;
mso-pagination:widow-orphan;
font-size:10.0pt;
font-family:"Times New Roman";
mso-ansi-language:#0400;
mso-fareast-language:#0400;
mso-bidi-language:#0400;}
</style>
<![endif]--><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]-->
</head>
<body lang=EN-US link=blue vlink=purple style='tab-interval:36.0pt'>
<div class=Section1>
<p class=MsoNormal><b style='mso-bidi-font-weight:normal'><font size=2
face=Arial><span style='font-size:10.0pt;font-family:Arial;font-weight:bold;
mso-bidi-font-weight:normal'>Reminder!!<o:p></o:p></span></font></b></p>
<p class=MsoNormal><font size=2 color=navy face=Arial><span style='font-size:
10.0pt;font-family:Arial;color:navy'><o:p> </o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'><o:p> </o:p></span></font></p>
<p class=MsoNormal><b style='mso-bidi-font-weight:normal'><font size=2
face=Arial><span style='font-size:10.0pt;font-family:Arial;font-weight:bold;
mso-bidi-font-weight:normal'>Guest Speaker<o:p></o:p></span></font></b></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'><o:p> </o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'>Presented by: <st1:City w:st="on">Toyota</st1:City>
Technological Institute at <st1:place w:st="on"><st1:City w:st="on">Chicago</st1:City></st1:place><o:p></o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'><o:p> </o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'><o:p> </o:p></span></font></p>
<p class=MsoNormal><b style='mso-bidi-font-weight:normal'><font size=2
face=Arial><span style='font-size:10.0pt;font-family:Arial;font-weight:bold;
mso-bidi-font-weight:normal'>Speaker: James Cheney<o:p></o:p></span></font></b></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'>Speaker’s home page:<span
style='mso-spacerun:yes'> </span><a
href="http://homepages.inf.ed.ac.uk/jcheney/">http://homepages.inf.ed.ac.uk/jcheney/</a><o:p></o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'><o:p> </o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'><o:p> </o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'>Date: Tuesday, April 17, 2007<o:p></o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'>Time: 10:00<o:p></o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'>Location: TTI-C Conference room<o:p></o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'><o:p> </o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'><o:p> </o:p></span></font></p>
<p class=MsoNormal><b style='mso-bidi-font-weight:normal'><font size=2
face=Arial><span style='font-size:10.0pt;font-family:Arial;font-weight:bold;
mso-bidi-font-weight:normal'>Title:</span></font></b><font size=2 face=Arial><span
style='font-size:10.0pt;font-family:Arial'> Nominal logic programming<o:p></o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'><o:p> </o:p></span></font></p>
<p class=MsoNormal><b style='mso-bidi-font-weight:normal'><font size=2
face=Arial><span style='font-size:10.0pt;font-family:Arial;font-weight:bold;
mso-bidi-font-weight:normal'>Abstract:<o:p></o:p></span></font></b></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'><o:p> </o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'>Syntactic proofs using structural induction principles are
essential for proving properties of formal systems (that is, metatheoretic
reasoning).<o:p></o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'>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.<span style='mso-spacerun:yes'> </span>In informal exposition
or reasoning, it is commonplace to resort to intuitive "without loss of
generality"<o:p></o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'>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.<o:p></o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'><o:p> </o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'>In completely formal proofs or implementations, it is not
possible to ignore these details; they must be addressed correctly.<span
style='mso-spacerun:yes'> </span>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":<o:p></o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'>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.<o:p></o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'><o:p> </o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'>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.<span style='mso-spacerun:yes'> </span>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.<o:p></o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'><o:p> </o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'>If you have any questions or would like to meet the speaker,
please contact Ponda Barnes at <a href="mailto:pondabarnes@tti-c.org">pondabarnes@tti-c.org</a><o:p></o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'>For future TTI-C events, please go to <a
href="http://ttic.uchicago.edu/cal/monrh.php">http://ttic.uchicago.edu/cal/monrh.php</a><o:p></o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'><o:p> </o:p></span></font></p>
<p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
font-family:Arial'><o:p> </o:p></span></font></p>
</div>
</body>
</html>