Programming in Linear Temporal Logic

Wolfgang Jeltsch

Institut für Informatik, Informations- und Medientechnik
Brandenburgische Technische Universität Cottbus

Thursday, 10 February 2011, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B126 (note the unusual room!)

Slides from the talk [pdf]

Abstract: There is a Curry-Howard Correspondence between Functional Reactive Programming (FRP) and a subset of Linear Temporal Logic (LTL). This talk shows how we can extend this Curry-Howard Correspondence to cover larger subsets of LTL or even complete LTL. The extensions of the correspondence give rise to extensions of FRP, namely mixing of continuous and discrete data as well as dataflow programming with an advanced type system.

ERDF
Tarmo Uustalu
Last update 10.2.2011