Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / SS 2010 / Oberseminar / Jan Hoffmann, Big-Step Operational Semantics and Divergence


Inhaltsbereich

Jan Hoffmann, Big-Step Operational Semantics and Divergence

28.05.2010 14:15
Wann 14:15 15:15 28.05.2010
von bis
Wo L109
Termin übernehmen vCal
iCal

  In its classic formulation, big-step operational semantics does not
 formalize evaluations that diverge.  This is problematic if one
 intends to proof statements for both terminating and non-terminating
 evaluations of programs.  

 We present three different big-step semantics for the lambda
 calculus to illustrate how big-step semantics can be used to
 formalize diverging computations.  The first (following Cousot et
 al.) uses additional coinductive rules, the second (following Leroy)
 interprets the usual rules coinductively, and the third adds
 additional inductive rules.

 To motivate the inductive approach we discuss the soundness proof of a
 static analysis that computes resource bounds for functional programs.

Artikelaktionen

abgelegt unter:

Funktionsleiste