/lambda-nq

Lambda calculus with catch/throw

Primary LanguageStandard MLMIT LicenseMIT

Lambda NQ

Lambda NQ with call-by-value, left-to-right evaluation.

Build

Prerequisites: MLKit or MLton, and cmyacc.

$ make mlkit

Or,

$ make mlton

Usage

$ ./lambda-nq [filename]

Examples

catch X : unit =>
  throw X () : bottom

catch X : unit =>
catch Y : bottom =>
  throw Y (throw X () : bottom) : bottom

The following is ill-typed because X is inaccessible inside the lambda abstraction:

catch X : unit -> unit =>
  fn x : unit =>
    throw X (fn y : unit => y) : unit

Reference

Yosuke Fukuda and Ryosuke Igarashi. A Reconstruction of Ex Falso Quodlibet via Quasi-Multiple-Conclusion Natural Deduction. Logic, Rationality, and Interaction, 2017. DOI.