Jan Hoffmann, Big-Step Operational Semantics and Divergence

  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.