[1]

William L. Harrison, Adam Procter and Gerard Allwein.
The confinement problem in the presence of faults.
In Proceedings of the 2012 International Conference on Formal
Engineering Methods, 2012.
[ bib 
.pdf ]
In this paper, we establish a semantic foundation for the safe
execution of untrusted code. Our approach extends Moggi's computational λcalculus in two dimensions with operations for asynchronous concurrency, shared state and software faults and with an effect type system a la Wadler providing finegrained control of effects. An equational system for fault isolation is exhibited and its soundness demonstrated with a semantics based on monad transformers. Our formalization of the equational system in the Coq theorem prover is discussed. We argue that the approach may be generalized to capture other safety properties, including information flow security.

[2]

Chris Hathhorn, Michela Becchi, William L. Harrison and Adam Procter.
Formal semantics of heterogeneous cudac: A modular approach with
applications.
In Proceedings of the 2012 Systems Software Verification
Conference, 2012.
[ bib 
.pdf ]
We extend an offtheshelf, executable formal semantics of C (Ellison and Rosiu's K Framework semantics) with the core features of CUDAC. The hybrid CPU/GPU computation model of CUDAC presents challenges not just for programmers, but also for practitioners of formal methods. Our formal semantics helps expose and clarify these issues. We demonstrate the usefulness of our semantics by generating a tool from it
capable of detecting some race conditions and deadlocks in CUDAC programs. We discuss limitations of our model and argue that its extensibility can easily
enable a wider range of verification tasks.

[3]

Gerard Allwein, William L. Harrison and David Andrews.
Simulation logic.
In Proceedings of the 2012 Conference on NonClassical Logics
(to appear), 2012.
[ bib 
.pdf ]
Simulation relations have been discovered in many areas: Computer Science, philosophical and modal logic, and set theory. However, the simulation condition is strictly a firstorder logic statement. We extend modal logic with modalities and axioms, the latter's modeling conditions are the simulation conditions. The modalities are normal, i.e., commute with either conjunctions or disjunctions and preserve either Truth or Falsity (respectively). The simulations are considered arrows in a category where the objects are descriptive, general frames. One can augment the simulation modalities by axioms for requiring the underlying modeling simulations to be bisimulations or to be pmorphisms. The modal systems presented are multisorted and both sound and complete with respect to their algebraic and Kripke semantics.

[4]

Adam Procter, William L. Harrison and Aaron Stump.
The design of a practical proof checker for a lazy functional
language.
In Proceedings of the 2012 Trends in Functional Programming
Conference (to appear), 2012.
[ bib 
.pdf ]
Pure, lazy functional languages like Haskell provide a sound basis for formal reasoning about programs in an equational style. In
practice, however, equational reasoning is underutilized. We suggest that part
of the reason for this is the lack of accessible tools for developing
machinechecked equational reasoning proofs. This paper outlines the design of
MProver, a system which fills just that niche. MProver features firstclass
support for reasoning about potentially undefined computations (particularly
important in a lazy setting), and an extended notion of Haskelllike type
classes, enabling a highly modular style of program verification that closely
follows familiar functional programming idioms.

[5]

Gerard Allwein and William L. Harrison.
A channel theoretic account of separation security.
In Proceedings of the 2011 International Conference on
Engineering Reconfigurable Systems and Algorithms (ERSA11), 2011.
[ bib 
.pdf ]
It has long been held that information flow security models should be organized with respect to a theory of information, but typically they are not. The appeal of a informationtheoretic foundation for information flow security seems natural, compelling and, indeed, almost tautological. This article illustrates how channel theorya theory of information based in logiccan provide a basis for noninterference style security models. The evidence presented here suggests that channel theory is a useful organizing principle for information flow security.

[6]

William L. Harrison, Benjamin Schulz, Adam Procter, Andrew Lukefahr, and Gerard
Allwein.
Towards semanticsdirected system design and synthesis.
In Proceedings of the 2011 International Conference on
Engineering Reconfigurable Systems and Algorithms (ERSA11), 2011.
[ bib 
.pdf ]
High assurance systems have been defined as systems “you would bet your life on.” This article discusses the application of a form of functional programmingwhat we call “monadic programming”to the generation of high assurance and secure systems. Monadic programming languages leverage algebraic structures from denotational semantics and functional programmingmonadsas a flexible, modular organizing principle for secure system design and implementation. Monadic programming languages are domainspecific functional languages that are both sufficiently expressive to express essential system behaviors and semantically straightforward to support formal verification.

[7]

Gerard Allwein, Yingrui Yang, and William L. Harrison.
Qualitative decision theory via channel theory.
Logic and Logical Philosophy, pages 81110, 2011.
Extended version of [8].
[ bib 
.pdf ]
We recast parts of decision theory in terms of channel theory
concentrating on qualitative issues. Channel theory allows one to move
between model theoretic and language theoretic notions as is necessary for
an adequate covering. Doing so clari?es decision theory and presents the
opportunity to investigate alternative formulations. As an example, we take
some of Savage's notions of decision theory and recast them within channel
theory. In place of probabilities, we use a particular logic of preference. We
introduce a logic for describing actions separate from the logic of preference
over actions. The structures introduced by channel theory that represent
the decision problems can be seen to be an abstract framework. This framework is very accommodating to changing the nature of the decision problems
to handle different aspects or theories about decision making.

[8]

Gerard Allwein, Yingrui Yang, and William S. Harrison.
Decision theory via channel theory.
In Proceedings of the Logic in Cognitive Science Conference,
2010, Logic and Logical Philosophy Journal. The Nicolaus Copernicus
University Press, 2010.
[ bib ]

[9]

Gerard Allwein and William L. Harrison.
Partiallyordered modalities.
In Advances in Modal Logic, pages 121, 2010.
[ bib 
.pdf ]
Modal logic is extended by partially ordering the modalities. The modalities are normal, i.e., commute
with either conjunctions or disjunctions and preserve either Truth or Falsity (respectively). The partial
order does not conflict with type of modality (K, S4, etc.) although this paper will concentrate on S4
since partially ordered S4 systems appear to be numerous. The partiallyordered normal modal systems
considered are both sound and complete. Hilbert and Gentzen systems are given. A cutelimination theorem
holds (for partially ordered S4), and the Hilbert and Gentzen systems present the same logic. The partial
order induces a 2category structure on a coalgebraic formulation of descriptive frames. Channel theory is
used to `move' modal logics when the source and target languages may be dierent. A particular partially
ordered modal system is shown to be applicable to security properties

[10]

W. Harrison, A. Procter, J. Agron, G. Kimmel, and G. Allwein.
Modeldriven engineering from modular monadic semantics:
Implementation techniques targeting hardware and software.
In DSL '09: Proc. of the IFIP TC 2 Working Conference on
DomainSpecific Languages, pages 2044, 2009.
[ bib 
.pdf ]
Recent research has shown how the formal modeling of concurrent systems can benefit from monadic structuring. With this approach, a formal system model is really a program in a domain specific language defined by a monad for sharedstate concurrency. Can these models be compiled into efficient implementations? This paper addresses this question and presents an overview of techniques for compiling monadic concurrency models directly into reasonably efficient software and hardware implementations. The implementation techniques described in this article form the basis of a semanticsdirected approach to modeldriven engineering.

[11]

William L. Harrison and James Hook.
Achieving information flow security through monadic control of
effects.
J. Comput. Secur., 17:599653, October 2009.
[ bib 
.pdf ]
This paper advocates a novel approach to the construction of secure
software: controlling information flow and maintaining integrity via
monadic encapsulation of effects. This approach is constructive,
relying on properties of monads and monad transformers to build,
verify, and extend secure software systems. We illustrate this
approach by construction of abstract operating systems called
separation kernels. Starting from a mathematical model of
sharedstate concurrency based on monads of resumptions and state, we
outline the development by stepwise refinements of separation kernels
supporting Unixlike system calls, interdomain communication, and a
formally verified security policy (domain separation). Because monads
may be easily and safely represented within any pure, higherorder,
typed functional language, the resulting system models may be directly
realized within a language such as Haskell.

[12]

William L. Harrison, Gerard Allwein, Andy Gill, and Adam Procter.
Asynchronous exceptions as an effect.
In Proceedings of the Mathematics of Program Construction
(MPC08), pages 153176, 2008.
[ bib 
.pdf ]
Asynchronous interrupts abound in computing systems, yet they remain a
thorny concept for both programming and verification practice.
The ubiquity of interrupts underscores the importance of developing
programming models to aid the development and verification of
interruptdriven programs.
The research reported here recognizes asynchronous interrupts as a
computational effect and encapsulates them as a building block in
modular monadic semantics.
The resulting modular semantic model can serve as both a guide for
functional programming with interrupts and as a formal basis for reasoning about
interruptdriven computation as well.

[13]

Pericles S. Kariotis, William L. Harrison, and Adam M. Procter.
Making monads firstclass with template haskell.
In Proceedings of the first ACM SIGPLAN Symposium on Haskell,
Haskell '08, pages 99110, New York, NY, USA, 2008. ACM.
[ bib 
.pdf ]
Monads as an organizing principle for programming and semantics are notoriously difficult to grasp, yet they are a central and powerful abstraction in Haskell. This paper introduces a domainspecific language, MonadLab, that simplifies the construction of monads, and describes its implementation in Template Haskell. MonadLab makes monad construction truly first class, meaning that arcane theoretical issues with respect to monad transformers are completely hidden from the programmer. The motivation behind the design of MonadLab is to make monadic programming in Haskell simpler while providing a tool for nonHaskell experts that will assist them in understanding this powerful abstraction.
Keywords: domainspecific languages, monads, staged programming

[14]

William L. Harrison and Adam Procter.
Cheap (but functional) threads.
Higher Order and Symbolic Computation (accepted for
publication).
45 pages. Available by request.
[ bib ]
This article demonstrates how a powerful and expressive abstraction
from concurrency theory plays a dual role as a programming tool
for concurrent applications and as a foundation for their verification.
This abstractionmonads of resumptions expressed using monad
transformersis cheap: it is easy to understand, easy to
implement, and easy to reason about.
We illustrate the expressiveness of the resumption monad with the
construction of an exemplary multitasking operating system kernel
with process forking, preemption, message passing, and
synchronization constructs in the pure functional programming
language Haskell.
Because resumption computations are streamlike structures, reasoning
about this kernel may be posed as reasoning about streams, a problem
which is wellunderstood. And, as an example, this article
illustrates how a liveness propertyfairnessis proven and
especially how the resumptionmonadic structure promotes such
verifications.

[15]

William Harrison.
Proof abstraction for imperative languages.
In Proceedings of the 4th Asian Symposium on Programming
Languages and Systems (APLAS06), pages 97113, 2006.
[ bib ]
Modularity in programming language semantics derives from abstracting over
the structure of underlying denotations, yielding semantic descriptions that are more abstract and reusable. One such semantic framework is Liang's modular
monadic semantics in which the underlying semantic structure is encapsulated with a monad. Such abstraction can be at odds with
program verification, however, because program specifications require access to the (deliberately) hidden semantic
representation. The techniques for reasoning about modular monadic definitions of imperative programs introduced here overcome this barrier.
And, just like program definitions in modular monadic semantics, our program specifications and proofs are representationindependent
and hold for whole classes of monads, thereby yielding proofs of great generality.

[16]

William L. Harrison.
The essence of multitasking.
In 11th International Conference on Algebraic Methodology and
Software Technology (AMAST 2006), pages 158172, July 2006.
[ bib 
.pdf ]
This article demonstrates how a powerful and expressive abstraction from concurrency theorymonads of resumptionsplays a dual rôle as a programming tool
for concurrent applications.
The article demonstrates how a
wide variety of typical OS behaviors may be specified in terms of
resumption monads known heretofore exclusively in the literature of
programming language semantics.
We illustrate the expressiveness of the resumption monad with the
construction of an exemplary
multitasking kernel in the pure functional language
Haskell.

[17]

X. Z. Fu, H. Wang, W. Harrison, and R. Harrison.
RNA pseudoknot prediction using term rewriting.
International Journal of Data Mining and Bioinformatics, 2005.
[ bib ]
RNA plays a critical role in mediating every step of cellular information transfer from genes to functional proteins. Pseudoknots are functionally important and widely occurring structural motifs found in all types of RNA. Therefore predicting their structures is an important problem. In this paper, we present a new RNA pseudoknot structure prediction method based on term rewriting. The method is implemented using the Mfold RNA/DNA folding package and the term rewriting language Maude. In our method, RNA structures are treated as terms and rules are discovered for predicting pseudoknots. Our method was tested on 211 pseudoknots in PseudoBase and achieves an average accuracy of 74.085 percent compared to the experimentally determined structure. In fact, most pseudoknots discovered by our method achieve an accuracy of above 90 percent. These results indicate that term rewriting has a broad potential in RNA applications ranging from prediction of pseudoknots to discovery of higher level RNA structures involving complex RNA tertiary interactions.

[18]

William L. Harrison and Richard B. Kieburtz.
The logic of demand in Haskell.
Journal of Functional Programming, 15(6):837891, 2005.
[ bib 
.pdf ]
Haskell is a functional programming language whose
evaluation is lazy by default. However, Haskell also
provides pattern matching facilities which add a
modicum of eagerness to its otherwise lazy default
evaluation. This mixed or nonstrict
semantics can be quite difficult to reason
with. This paper introduces a programming logic,
PLogic, which neatly formalizes the mixed
evaluation in Haskell patternmatching as a logic,
thereby simplifying the task of specifying and
verifying Haskell programs. In PLogic, aspects of
demand are reflected or represented within both the
predicate language and its model theory, allowing
for expressive and comprehensible program
verification.

[19]

William Harrison.
A simple semantics for polymorphic recursion.
In Proceedings of the 3rd Asian Symposium on Programming
Languages and Systems (APLAS05), pages 3751, Tsukuba, Japan, November
2005.
[ bib 
.pdf ]
Polymorphic recursion is a useful extension of Hindley
Milner typing and has been incorporated in the functional programming
language Haskell. It allows the expression of efficient algorithms
that take advantage of nonuniform data structures and provides key
support for generic programming. However, polymorphic recursion is,
perhaps, not as broadly understood as it could be and this, in part,
motivates the denotational semantics presented here. The semantics reported
here also contributes an essential building block to any semantics
of Haskell: a model for firstorder polymorphic recursion. Furthermore,
Haskellstyle type classes may be described within this semantic framework
in a straightforward and intuitively appealing manner.

[20]

X. Z. Fu, H. Wang, W. Harrison, and R. Harrison.
RNA pseudoknot prediction using term rewriting.
In Proceedings of IEEE Fifth Symposium on Bioinformatics and
Bioengineering (BIBE05), pages 169176, Minneapolis, MN, October 2005.
[ bib 
.pdf ]
RNA plays a critical role in mediating every step of cellular information transfer from genes to functional proteins. Pseudoknots are widely occurring structural motifs found in all types of RNA and are also functionally important. Therefore predicting their structures is an important problem. In this paper, we present a new RNA pseudoknot prediction model based on term rewriting rather than on dynamic programming, comparative sequence analysis, or contextfree grammars. The model we describe is implemented using the Mfold RNA/DNA folding package and the term rewriting language Maude. Our model was tested on 211 pseudoknots in PseudoBase and achieves an average accuracy of 74.085% compared to the experimentally determined structure. In fact, most pseudoknots discovered by our method achieve an accuracy of above 90%. These results indicate that term rewriting has a broad potential in RNA applications from prediction of pseudoknots to higher level RNA structures involving complex RNA tertiary interactions.

[21]

William Harrison and James Hook.
Achieving information flow security through precise control of
effects.
In 18th IEEE Computer Security Foundations Workshop (CSFW05),
pages 1630, AixenProvence, France, June 2005.
[ bib 
.pdf ]
This paper advocates controlling information flow and maintaining integrity via monadic encapsulation of effects. This approach is constructive, relying on properties of monads and monad transformers to build, verify, and extend secure software systems. We illustrate this approach by construction of abstract operating systems called separation kernels.

[22]

William L. Harrison and Robert W. Harrison.
Domain specific languages for cellular interactions.
In Proceedings of the 26th Annual IEEE International Conference
on Engineering in Medicine and Biology (EMBC04), September 2004.
[ bib 
.pdf ]
Bioinformatics is the application of Computer Science techniques to problems in Biology, and this paper explores one such application with great potential: the modeling of life cycles of autonomous, intercommunicating cellular systems using domainspecific programming languages (DSLs). We illustrate this approach for the simple photosynthetic bacterium R. Sphaeroides with a DSL called CellSys embedded in the programming language Haskell.

[23]

William Harrison, Mark Tullsen, and James Hook.
Domain separation by construction.
In LICS03 Satellite Workshop on Foundations of Computer Security
(FCS03), June 2003.
21 pages.
[ bib 
.pdf ]
This paper advocates a novel approach to languagebased security: by structuring software with monads (a form of abstract data type for effects), we are able to maintain separation of effects by construction. The thesis of this work is that wellunderstood properties of monads and monad transformers aid in the construction and verification of secure software. We introduce a formulation of noninterference based on monads rather than the typical tracebased formulation. Using this formulation, we prove a noninterference style property for a simple instance of our system model. Because monads may be easily and safely represented within any pure, higherorder, typed functional language, the resulting system models may be directly realized within such a language.

[24]

William Harrison and Richard Kieburtz.
Patterndriven reduction in haskell.
In 2nd International Workshop on Reduction Strategies in
Rewriting and Programming (WRS02), Copenhagen, Denmark, 2002.
[ bib 
.pdf ]
Haskell is a functional programming language with nominally nonstrict
semantics, implying that evaluation of a Haskell expression proceeds by
demanddriven reduction. However, Haskell also provides pattern
matching
on arguments of functions, in let expressions and in the match
clauses of case expressions. Patternmatching requires
datadriven reduction to the extent necessary to
evaluate a pattern match or to bind variables introduced in a pattern.
In this paper we
provide both an abstract semantics and a logical characterization of
patternmatching in Haskell and the reduction order that it entails.

[25]

William Harrison, Timothy Sheard, and James Hook.
Fine control of demand in Haskell.
In 6th International Conference on the Mathematics of Program
Construction (MPC02), Dagstuhl, Germany, volume 2386 of Lecture Notes
in Computer Science, pages 6893. SpringerVerlag, 2002.
[ bib 
.pdf ]
Functional languages have the lambda calculus at their core, but then depart from this firm foundation by including features that alter their default evaluation order. The resulting mixed evaluationpartly lazy and partly strictcomplicates the formal semantics of these languages. The functional language Haskell is such a language, with features such as patternmatching, case expressions with guards, etc., introducing a modicum of strictness into the otherwise lazy language. But just how does Haskell differ from the lazy lambda calculus? We answer this question by introducing a calculational semantics for Haskell that exposes the interaction of its strict features with its default laziness. In the semantics, features perturbing Haskell's standard lazy evaluation order are specified computationally (i.e., monadically) rather than as pure values (i.e., functions, scalars, etc.).

[26]

Bill Harrison and Tim Sheard.
Dynamically adaptable software with metacomputations in a staged
language.
In Proceedings of the Second International Workshop on
Semantics, Applications, and Implementation of Program Generation (SAIG),
volume 2196 of Lecture Notes in Computer Science, pages 163182,
Florence, Italy, 2001. SpringerVerlag.
[ bib 
.pdf ]
Profiledriven compiler optimizations take advantage of information gathered at runtime to recompile programs into more efficient code. Such optimizations appear to be more easily incorporated within a semanticsdirected compiler structure than within traditional compiler structure. We present a case study in which a metacomputationbased reference compiler for a small imperative language converts easily into a compiler which performs a particular profiledriven optimization: local register allocation. Our reference compiler is implemented in the staged, functional language MetaML and takes full advantage of the synergy between metacomputationstyle language definitions and the staging constructs of MetaML. We believe that the approach to implementing profiledriven optimizations presented here suggests a useful, formal model for dynamically adaptable software.

[27]

William Harrison.
Modular Compilers and Their Correctness Proofs.
PhD thesis, University of Illinois at UrbanaChampaign, 2001.
[ bib 
.pdf ]
This thesis explores the construction and correctness of modular compilers. Modular compilation is a compiler construction technique allowing the construction of compilers for highlevel programming languages from reusable compiler building blocks. Modular compilers are defined in terms of denotational semantics based on monads, monad transformers, and a new model of staged computation called metacomputations. A novel form of denotational specification called observational program specification and related proof techniques are developed to assist in modular compiler verification. It will be demonstrated that the modular compilation framework provides both a level of modularity in compiler proofs as well as a useful organizing principle for such proofs.

[28]

William Harrison and Samuel Kamin.
Metacomputationbased compiler architecture.
In 5th International Conference on the Mathematics of Program
Construction, Ponte de Lima, Portugal, volume 1837 of Lecture Notes in
Computer Science, pages 213229. SpringerVerlag, 2000.
[ bib 
.pdf ]
This paper presents a modular and extensible style of language specification based on metacomputations. This style uses two monads to factor the static and dynamic parts of the specification, thereby staging the specification and achieving strong bindingtime separation. Because metacomputations are defined in terms of monads, they can be constructed modularly and extensibly using monad transformers. Consequently, metacomputationstyle specifications are modular and extensible. A number of language constructs are specified: expressions, controlflow, imperative features, block structure, and higherorder functions and recursive bindings. Because of the strong bindingtime separation, metacomputationstyle specification lends itself to semanticsdirected compilation, which we demonstrate by creating a modular compiler for a blockstructured imperative, while language.

[29]

William L. Harrison and Samuel N. Kamin.
Modular compilers based on monad transformers.
In Proceedings of the 1998 International Conference on Computer
Languages, pages 122131. IEEE Computer Society Press, 1998.
[ bib 
.pdf ]
The monadic style of language specification has the
advantages of modularity and extensibility: it is
simple to add or change features in an interpreter to
re ect modifications in the source language. It has
proven difficult to extend the method to compilation.
We demonstrate that by introducing machinelike stores
(code and data) into the monadic semantics and then
partially evaluating the resulting semantic
expressions, we can achieve many of the same advantages
for a compiler as for an interpreter. A number of
language constructs and features are compiled:
expressions, CBV and CBN evaluation of
λexpressions, dynamic scoping, and various
imperative features. The treatment of recursive
procedures is outlined as well. The resulting method
allows compilers to be constructed in a mixandmatch
fashion just as in a monadstructured interpreter.

[30]

William Harrison.
Mechanizing the axiomatic semantics for a programming language with
asynchronous send and receive in hol.
Master's thesis, University of California, Davis, 1992.
[ bib 
.pdf ]
This thesis presents the axiomatic semantics for a simple distributed language and its mechanization in HOL. The constructs of this language include asynchronous send and synchronous receive statements as well as those basic to a sequential programming language. The language has the appearance of a system programming language that supports sequential execution extended with messagepassing, and would be a suitable basis for coding distributed operating systems. Included in the mechanization are functions which generate the goals associated with the verification of simple statements in the language.

[31]

William Harrison, Karl Levitt, and Myla Archer.
An hol mechanization of the axiomatic semantics of a simple
distributed programming language.
In Proceedings of the International Workshop on HigherOrder
Logic Theorem Proving and Its Applications, pages 347358, Leuven, Belgium,
September 1992.
[ bib ]

[32]

William Harrison and Karl Levitt.
Mechanizing security in HOL.
In Proceedings of the 1991 International Workshop on the HOL
Theorem Proving System and its Applications, pages 6366, Davis,
California, 1991. IEEE Computer Society Press.
[ bib ]

[33]

William Harrison, Karl Levitt, and Myla Archer.
Towards a Verified Code Basis for a Secure Distributed Operating
System.
Technical Report CSE9219, University of California at Davis, 1992.
[ bib ]

[34]

William Harrison.
Mechanizing the Axiomatic Semantics for a Programming Language with
Asynchronous Send and Receive in HOL.
Technical Report CSE9220, University of California at Davis, 1992.
[ bib ]

This file was generated by
bibtex2html 1.96.
