A proof method, subgoal induction, is presented as an alternative or supplement to the commonly used inductive assertion method. Its major virtue is that it can often be…
Ben Wegbreit
Author Archives
Faster retrieval from context trees
Context trees provide a convenient way of storing data which is to be viewed as a hierarchy of contexts. This note presents an algorithm which improves on previous…
One means of analyzing program performance is by deriving closed-form expressions for their execution behavior. This paper discusses the mechanization of such analysis,…
The treatment of data types in EL1
In constructing a general purpose programming language, a key issue is providing a sufficient set of data types and associated operations in a manner that permits both…
The synthesis of loop predicates
Current methods for mechanical program verification require a complete predicate specification on each loop. Because this is tedious and error prone, producing a program…
A model and stack implementation of multiple environments
Many control and access environment structures require that storage for a procedure activation exist at times when control is not nested within the procedure activated.…
Shape the Future of Computing
ACM encourages its members to take a direct hand in shaping the future of the association. There are more ways than ever to get involved.
Get Involved