Document Type thesis Author Name King, Christopher T. URN etd-042908-133033 Title An Axiomatic Semantics for Functional Reactive Programming Degree MS Department Computer Science Advisors Kathi Fisler, Advisor Michael Gennert, Department Head Dan Dougherty, Reader Keywords coq monads functional reactive programming formal verification Date of Presentation/Defense 2008-05-04 Availability unrestricted Abstract
Functional reactive programming (FRP) is a paradigm extending functional languages with primitives which operate on state. Typical FRP systems contain many dozens of such primitives. This thesis aims to identify a minimal subset of primitives which captures the same set of behavior as these systems, and to provide an axiomatic semantics for them using first-order linear temporal logic, with the aim of utilizing these semantics in formal verification of FRP programs. Furthermore, we identify several important properties of these primitives and prove that they are satisfied using the Coq proof assistant.
Files cking.pdf
Browse by Author | Browse by Department | Search all available ETDs
![[WPI]](/Buttons/seal.gif){kind=small}
![[Library]](/Academics/Library/Buttons/lib.gif){kind=small}
![[Home]](/Buttons/home.gif){kind=small}
![[Top]](/Buttons/top.gif){kind=small}