Faculty of Computing and Information Science >
Computing and Information Science >
Computing and Information Science Technical Reports >
Please use this identifier to cite or link to this item:
|Title: ||Generating event logics with higher-order processes as realizers|
|Authors: ||Bickford, Mark|
|Issue Date: ||25-Aug-2011|
|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.|
|Appears in Collections:||Computing and Information Science Technical Reports|
Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.