[Colloquium] Correction: [CS] Talk by Robert Harper, Carnegie Mellon University, 6/27/05

[Margery Ishmael]

PLEASE NOTE: This talk will take place in Ryerson 276 (annex) and not 
in Ryerson 251 as originally stated.

Begin forwarded message:

> From: Margery Ishmael <marge at cs.uchicago.edu>
> Date: June 23, 2005 4:04:16 PM CDT
> To: colloquium at cs.uchicago.edu
> Cc: cs at cs.uchicago.edu
> Subject: [CS] Talk by Robert Harper, Carnegie Mellon University, 
> 6/27/05
>
> DEPARTMENT OF COMPUTER SCIENCE
>
> Date: Monday, June 27, 2005
>
> Time: 2:00 p.m.
> Place: Ryerson 276 (Annex)
>
> -------------------------------------------
>
> Speaker:  ROBERT HARPER, Carnegie Mellon University
>
> Url:  http://www-2.cs.cmu.edu/~rwh/
>
> Title:  Mechanizing Metatheory Using Twelf
>
> Abstract:
>
> What does it mean for a programming language to exist?  The usual
> approach is to define a language by a "reasonably precise" description
> a la K&R, together with a "reference compiler" that implements it (and
> serves as the final arbiter of ambiguities).  This relies heavily on
> social constructs such as standardization committees, or on the
> marketing clout of a large corporation, and is not suitable as a basis
> for a rigorous analysis of the safety or security properties of the
> language.
>
> Another approach is to define a language by a rigorous semantics that
> is amenable to mathematical analysis.  The most successful method of
> semantic definition is to give a static semantics in the form of a
> type system and a dynamic semantics in the form of execution rules for
> a program.  This gives the definition an objective character that is
> amenable to analysis, and helps to ensure the compatibility of
> compilers for it.  But having a rigorous definition is not enough; at
> a minimum one must prove that it is internally coherent according to
> various criteria.  This re-introduces some of the difficulties of the
> traditional methods, because someone has to do the proofs and someone
> has to read them to ensure they are right.  The burdens of doing "at
> scale" are so severe that the semantics becomes an inhibitor, rather
> than an enabler, of innovation.
>
> One way forward is to formalize the definition within a logical
> framework and to use verification tools to check crucial properties,
> much as we use type systems to ensure sensibility of our programs.  I
> will describe the work we have been doing on mechanizing formal
> language definitions, and describe some of the successes, and
> difficulties, of using the Twelf system to verify their metatheory.
>
> Joint work with Karl Crary and Michael Ashley-Rolman.
>
> -------------------------------------------------------
>
> Host: David B. MacQueen
>
> *Refreshments will be served after the talk in Ryerson 255*
>
> People in need of assistance should call 773-834-8977 in advance.
>
>

=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Margery Ishmael
Secretary to the Chairman
Department of Computer Science
The University of Chicago
1100 E. 58th Street, Chicago, IL. 60637-1581
tel. 773.834.8977 fax. 773.702.8487
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/enriched
Size: 3333 bytes
Desc: not available
Url : http://mailman.cs.uchicago.edu/pipermail/colloquium/attachments/20050623/3c52ec74/attachment.bin