Generating Event Logics with Higher-Order Processes as Realizers
[PDF]
by Mark Bickford, Robert Constable, and David Guaspari
Cornell Tech Report URI: http://hdl.handle.net/1813/23562
Abstract
Our topic is broadening a practical "proofs-as-programs" method of program
development to "proofs-as-processes". We extend our previous results that
implement proofs-as-processes for the standard model of asynchronous message
passing computation to a much wider class of process models including
the π-calculus and other process algebras. Our first result is a
general process model whose definition in type theory is interesting
in itself both technically and foundationally. Process terms are type free
lambda-terms. Typed processes are elements of a co-inductive type. They are
higher-order in that they can take processes as inputs and produce them
as outputs.
A second new result is a procedure to generate event structures over the
general process model and then define event logics and event classes over
these structures. Processes are abstract realizers for assertions in the
event logics over them, and they extend the class of primitively realizable
propositions built on the propositions-as-types principle. They also provide
a basis for the third new result, showing when programmable event classes
generate strong realizers that prevent logical interference as processes
are synthesized.
