Logik-Sem., 19.04.06, B. Pientka
Uwe Waldmann
Einladung zum Vortrag
Zeit: Mittwoch, 19.04.06, 16.15 Uhr
Ort: Hörsaal 024, MPI Saarbrücken (Geb. E1.4)
Brigitte Pientka (McGill University, Montreal):
Contextual Modal Type Theory: A Foundation for Meta-variables
Zusammenfassung:
In recent years, higher-order reasoning systems and logical frameworks
have matured and been successful in several applications such as
proof-carrying code. Maybe surprisingly, there are still some
foundational and implementation issues which are poorly understood.
In this talk, we concentrate on the notion of meta-variables and their
role in higher-order unification. Both concepts are fundamental to proof
search, type reconstruction, efficient data-structures for higher-order
terms, and representation of incomplete proofs. First, we will present
a contextual modal type theory which provides an elegant, uniform
foundation for understanding meta-variables and explicit substitutions.
Second, we will sketch applications in higher-order patter unification.
This will provide new insights for efficient implementation strategies
and justifies logically design decisions which have so far been largely
motivated operationally. Finally, we will briefly discuss applications
of this work to compute the most specific generatlization of two terms
and its use in higher-order substitution tree indexing.
______________________________________________________________________
Das Logikseminar ist eine gemeinsame Veranstaltung des DFKI, des MPI
und der Fachrichtungen Informatik, Philosophie und Rechtswissenschaft.
Vortragswünsche bitte an Uwe Waldmann, MPI, Tel.: (0681) 9325-205,
uni-intern: 92205, E-Mail: u...@mpi-sb.mpg.de