(Draft) Tuesday Seminar

10 December 2002

by Thomas Hallgren

Highlights from the Workshop on Termination and Type Theory
Workshop on Termination and Type Theory
A session is about to start
Some interesting talks
Conor McBride: Seeing and Doing
Conor McBride: Seeing and Doing
Example: sorting by structural recursion
Sorting efficiently
Sorting efficiently with structural recursion
Sorting efficiently with structural recursion
From doing to seeing
From doing to seeing
Ana Bove: Modelling General Recursion in Type Theory
General recursion in type theory
General recursion in type theory
An example
An example
An example
What about mutual recursion?
What about nested recursion
What about nested recursion
A non-trivial example: Unification
Unification
Termination?
Domain predicate
Proofs
Yves Bertot: Type-theoretic functional semantics
The language IMP
Operational Semantics
Denotational Semantics
Denotation of Commands
Denotation of Commands
Relating the two semantics
Relating the two semantics
Program extraction
Other talks
Conclusions

[

|

]