Date: 2015-04-27
Categories: research

Why operational models?

Why give operational specifications and proofs? Why not prefer, say, a program logic?

Most of my work focuses on operational models of programs, and operational proofs about these models. It is much more common to develop program logics and perform proofs in the logic. There are some reasons to prefer operational models and proofs:

Related articles:

  • 2018-06-14 A typed DSL for parsing
  • 2018-05-30 Potential improvements in filesystem performance
  • 2018-05-22 First Python program: an Earley parser!
  • 2018-02-01 New OCaml library: path resolution
  • 2017-09-06 ICFP most influential paper from 10 years ago
  • 2017-03-16 tjr-btree: a CoW B-tree library in OCaml
  • 2015-04-27 Why operational models?
  • 2014-11-26 Isabelle on 64bit ubuntu with 32bit libraries