[Colloquium] JOSE MESEGUER on Friday, December 10, 2004

[Margery Ishmael]

DEPARTMENT OF COMPUTER SCIENCE

Date: Friday, December 10, 2004

Time: 2:00 p.m.
Place: Ryerson 251

-------------------------------------------

Speaker:  JOSE MESEGUER

From:  CS Dept., Univ. of Illinois at Urbana-Champaign
       (currently visiting the CS Dept. Univ. of Chicago)

Url:  http://www.cs.uiuc.edu/people/faculty/meseguer.html

Title:  An Introduction to Maude

Abstract:

Maude is both a declarative language and an executable formal 
specification
language.  Maude modules are logical theories.  A Maude functional 
module
is an equational theory (\Sigma,E) where the equations E are 
Church-Rosser.
A Maude system module (the most general kind) is a rewrite theory of the
form (\Sigma,E,R), where the subcomponent (\Sigma,E) is an equational 
theory
with E Curch-Rosser, and R is a collection of non-functional rewrite 
rules
understood as local concurrent transitions of the system specified by 
the
theory.

Maude's equational logic (membership equational logic (MEL)) is quite
expressive: it supports subtype polymorphism, function overloading,
and partial functions.  Parameterized modules provide the analogue of
parametric polymorphism.  The talk will use a series of examples to
introduce the two logics (MEL and rewriting logic), and different
language features such as:

- rewriting modulo associativity, commutativity, and identity axioms,
- breadth first search
- LTL model checking

The examples will also give some flavor for some applications.

The style will be highly informal, focusing primarily on examples and
features.  If there is interest and time permits, I will also discuss
briefly other important feaures such as evaluation strategies and
logical reflection.

-------------------------------------------------------

Host: David B. MacQueen

*Refreshments will be served at the talk*

People in need of assistance should call 773-834-8977 in advance.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/enriched
Size: 1979 bytes
Desc: not available
Url : http://mailman.cs.uchicago.edu/pipermail/colloquium/attachments/20041207/13a5b6ac/attachment.bin