Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / SS 2011 / Oberseminar / Vladimir Komendantsky: A method of nested induction-coinduction illustrated on recursive subtyping.


Inhaltsbereich

Vladimir Komendantsky: A method of nested induction-coinduction illustrated on recursive subtyping.

TCS Oberseminar, 01.07.2011 11:15 Uhr
Wann 11:15 12:30 01.07.2011
von bis
Wo L109
Name
Termin übernehmen vCal
iCal

I am interested in certian kinds of subtype and containment relations and
their decision algorithms. A formal definition of a relation is required in a
theorem prover, for example, for establishing a verified soundness and
completeness result for a decision algorithm. In the talk, I describe a
formalisation of a recursive subtype relation by using a method of nested
induction-coinduction in the proof assistant Coq. Thus the subtype relation is
not merely a semantic relation on tree interpretations of types, but the
required syntactic relation on types.

Artikelaktionen

abgelegt unter:

Funktionsleiste