David Martin Papers

David Martin Papers

In 1997, the UCR Libraries received the entire library and personal papers of Dr. David F. Martin.  This collection was well over 40 boxes of books, journals, reprints, technical reports, syllabi, etc...

When all of the books and journals were processed, I was left with boxes and boxes of articles and technical reports that I couldn't do much with, because they don't meet the criteria of our collection, but that I couldn't bring myself to toss. I have discarded a large number of obvious journal reprints and technical reports that have shown up online, but this site represents the 8 remaining boxes.

These are some of the reprints and technical reports.


Title Notes
A Case Study: Modelling Protocols in Higher Order Logic no sign in google
A Comparison of Formal Security Policy Models Haigh, J. T., 7th DoD/NBS Computer Security Conference, pp. 88-111, NBS/NCSC, September 1984.
A Computer Proof of the correctness of a Simple Optimizing Compiler for Expressions SRI Technical Report 5. 1977
A Data Type Theory Greiter, 1982 ACM Sigplan Notices
A Debugger for Ada Tasking Brindle; Aerospace corporation ATR-85(8033)-1 and IEEE Transactions on software Engineering 15(3):293 (1993)
A Denotational Definition of the Programming language pascal Tennant, 1977 Oxford Technical Report Queens College
A Detailed Analysis of Gallager, Humblet, and Spira's distributed minimum-weight spanning tree algorithm Stomp, cited once on Google.
A direct Report of the Church-Rosser Theorem Lehmann 1973 Brown University
A Lambda-Calculus for Parallel Functions Boudol INRIA 1231 1990 and Information and Computation 108(1):51
A Language-Oriented Approach to Computer Architecture Wilcox TR 191, 1980 CSL Stanford
A Lattice structured proof technique applied to a minimum spanning tree algorithm Welch, ACM Proceedings.
A Lazy Evaluator Peter Henderson. ACM SIGACT-SIGPLAN
A Library for Visualizing Combinatorial Structures SRC Research Report 128a; Najork
A Logical View of Composition Abadi, 1992
A Machine Independent Algorithm for Code Generation and its Retargetable Compilers Glanville UCB-CS-78-01, ERL - M78/9
A nanoAVA Definition Craigen, CLI 21
A Package for inductive relation definitions in HOL Melham HOL Theorem Provem
A Programming Language for the 360 computers Wirth Stanford CS 53 1967
A Proof of the Correctness of a Simple Parser of Expressions by the Boyer-Moore System Gloess, SRI N00014-75-C-0816-SRI-7
A Proof Rule for Euclid Procedures ISI/RR-77-60, USC; Guttag
A Proof Rule for Functions ISI/RR-77-62 USC; Musser
A Proposition for a Theory of Testing: An Abstract Approach to the Testing Process Aarhus DAIMI PB-160; Bouge
A Self-Referral Language Definition The Royal Institute of TEchnology TRITA-CS-8604
A Simple Lambda Calculus Model of Programming Languages NYU Courant Institute COO-3077-28; Abdali
A Simple Precedence Grammar for Algol '68 Chirica UCLA Mod. & Meas. Note #10 1972
A Structural Approach to Operational Semantics DAIMI FN-19 1981 Arhaus; Plotkin
A Technique for Modelling Higher Order Data Types no sign in google
A Theory of Asynchronous Circuits III Bartkey, UI Report 96
A Verified Code Generator for a Subset of Gypsy Young, TR 33 CLI
A Verified Compiler for a structured Assembly Language Curzon, HOL Theorem Proving
A Verified Specification of a Hierarchical Operating System Saxena TR 107 SU-SEL-76-011 Digital Systems Lab Stanford
Abstract Errors for abstract data types Goguen, J.A.: Abstract Errors for Abstract Data Types. Proc. Conf. on Formal Description of Programming Concepts. Neuhold, E.J. (ed.). Amsterdam: North-Holland, 1978
ACT One: An Algebraic Specification Language with two levels of semantics H. Ehrig, W. Fey, and H. Hansen. ACT ONE: An Algebraic Specification Language with two Levels of Semantics. Technical Report 83-01, TUB, Berlin, 1983.
ACV: An Arithmetic Circuit Verifier Chan, 1996. ACM IEEE CAD
Ada Concrete and Abstract Syntax no sign in google
Algebraic Semantics for ALGOL 68 "Algebraic Semantics for ALGOL 68," with Daniel Berry, Modelling and Measurement Note Number 29, Computer Science Department, University of California at Los Angeles, September 1974.
Algorithm Verification Maurer ERL-M290 1971
An Analysis of U.S. Patent #5,243,538 "Comparison and Verification System for Logic Circuits and Method Thereof," Bryant 1994,
An Algebraic Specification of a Pascal Compiler Joelle Despeyroux 1983 INRIA no 209 and ACM Sigplan Notices 18/12/34
An Approach to Systems Verification Bevier, CLI Technical Report 41 1989 also Journal of Automated Reasoning.
An Approach to Compiler Correctness Using Interpretation Between Theories Levy, Aerospace Corporation ATR-86(8454)-4 also Dissertation for UCLA
An Efficient Evaluator for Attribute Grammars with Conditional Rules Jean H. Gallier. An efficient evaluator for Attribute Grammars with Conditional Rules. Technical report, Computer and Information Sciences Department, University of  Pennsylvania, Philadelphia, PA, 1985. 
An Interactive Program Verification system ISI/RR-74-22 USC; Good
An Introduction to Action Semantics in book: Logic and algebra of specification
An Optimal Algorithm for the Abstract Continuation-Passing style transformation no sign in google
Arbitrarily large continuous algebras on one generator
Attribute-Influenced LR Parsing Aarhus Daimi-PB-119; Jones
Authentication in the Taos Operating System SRC Research Report 117; Wobber
Automated Proofs of Object code for a Widely Used Microprocessor SRC Research Report 114; Yu
Automatic Generation of Syntax-Repairing and Paragraphing Parsers Barnard, CSRG-52 1975 U Toronto
Bit-Level Analyis of an SRT Divider Circuit
Building friendly parsers
Category Theoretical Logics and algebras of Programs Goteborg; Dybjer
Checking a Large Routine  in ISBN:0-262-23136-0
Commentary on The Mathematical Semantics of Algol 60 no sign in google
Compiling UC using source-to-source transformations
Completeness of many-sorted Equational logic
Computer System Security Evaluation
Concurrent Programming with events: The Concurrent ML Manual (0.9) .9.6 is online in Postscript :
Conditional Rewrite Rules as an Algebraic Semantics of Processes Badouel INRIA 1226 1990
Conjoining Specifications SRC Research Report 118; Abadi
Constructive methods on Porgram Verification
Continuous Semilattices
CPL Elementary Programming Manual
Description of /360 WATFOR A Fortran Compiler Cress CSTR-1000U Waterloo
Digital Circuit Verification using Partially-Ordered State Models
Distributed Garbage Collection for Network Objects SRC Research Report 116; Birrell
Equational Logic - Walter Taylor
Equations and Rewrite rules : a survey
Equations in a Space of Languages Blikle, Warszawa 1971 43 CC Pas Reports
Exploiting symmetry in temporal logic model checking
Extended Abstract for the paper A New Rule for Loop Verification no sign in google
Extensible Syntax with Lexical Scoping SRC Research Report 21; Cardelli
Fixed Point Semantics and Dijkstra's Fundamental Invariance Theorem Stichting Mathematisch Centrum. Informatica, No. ; IW 29/75
Formal Semantics (J.C. Reynolds - Preliminary draft) no sign in google
Formal Semantics by a Combination of Denotational Semantics and high-Level Petri Nets Aarhus DAIMI PB-152; Hansen
Formal Verification of Mathematical Software Odyssey Research Assoc., Inc RADC-TR-90-%# Vol II
Formal Verification of Programs CMU SEI-CM-20-1.0 Curriculum module
Formal Verification of the gigamax cache consistency protocol
Formally Verifying a microprocessor using a simulation methodology
Foundations of the Theory of Algorithms, I Moschovakis, UCLA
Functional programming using Caml Light
HOL - A Machine Oriented Formulation of Higher Order Logic Gordon, 1987 Cambridge
How to Write a Long Formula SRC Research Report 119; Lamport
Implementation f a Parallel Processing Language Bernstein GE 67-C-080 1967
Implementing prolog compiling predicate logic programs Warren, D.H., 1-May-77, University of Edinburgh Dept. of AI Technical Reports #39-40.
Inside Hector: The Systems View SRC Research Report 123; Reid
Introducing OBJ Or in CiteSeer
Lis as Object Code for an ADA-0 Translator : Case Study no sign in google
Lisp Programming and Proving
Local Area Network Implementation Plan Naylor SD-TR-85-83
Digital Termination System for Extended Carriers Local Digital Distribution Company 1981
Logic Programming and Parsers for Extended Context Free Grammars no sign in google
Machine Independent Code Generation Kozlak TR CSRG-125 U Toronto 1981
Macro Tree Transducers Technische Hogeschool Twente INF-82-7; Engelfriet
Making Denotational Semantics Less concrete Mosses, P.D. In: Proc. Int. Workshop on Semantics of Programming Languages, Bad Honnef. Bericht 41, Abteilung Informatik, Universität Dortmund, 102-109 (1977).
Many-sorted theories and their algebras with some applications to data types Algebraic methods in semantics Cambridge University Press New York, NY, USA ©1986
Mathematical Semantics of Programming Languages Queens U. Kingston, Ont. TR 73-15 1973
Mechanical Methods for Proving Poperties of Recursive Computer Programs no sign in google
Mesa Language Manual Version 5.0 Xerox
Methodology for the Automatic Generation of Program Test Data Howden 1974 TR #41, published without the word "automatic" in 1975: IEEE Transactions on Computers c-24(5):554
Methods for Computing LALR(k) Lookahead Aarhus DAIMI PB-101; Kristensen
Microcode Verification Project Users Manual Crocker ISI/WP-18 USC
Microcode Verification Project Final Report Crocker ISI/WP-17.2 USC
Model checking and abstraction
Multipliers and dividers: Insights on Arithmetic  Circuit Verification (Extended Abstract)*
Natural Semantics on the Computer INRIA 416 Clement
Network Objects SRc Research Report 115; Birrell
Nth Root Computing Methods D. Martin - 1963 - UCLA Engineering 63-18. At SRLF already. Online.  Discarded.
Obliq: a Language with Distributed Scope SRC Research Report 122; Cardelli
On the Axiomatic Verification of Concurrent Algorithms Lengauer CSRG-94 1978 U Toronto

On the Completeness of the Inductive Assertion Method

Mathematische Centrum IW 12/73 ; De Bakker
On the Correctness of Refinement Steps in Program Development Helsinki CS A-1978-4; Back
On the Design and Verification of Operating Systems Flon Carnegie-Mellon (Dissertation)
On the Expressive Power of Attribute Grammars
On the Reduced Matrix Representation of LR(k) Parser Tables Joliat CSRG-28 1973 U Toronto
On Using Edinburgh LCF to Prove the Correctness of a Parsing Algorithm Cohn. Cambridge TR-20 Edinburgh CSR-113-82
Operational Semantics and Polymorphic Type Interference Tofte, Edinburgh. CST-52-88, ECS-LFCS-88-54
Operational Semantics of a Distributed Object-Oriented Language and its Z Formal Specification Benveniste INRIA 1230, 1990
Parameter passing in algebraic specification languages
Parsing tree languages using bottom-up tree automata with tree pushdown stores JH Gallier and KM Schimpf, Parsing Tree Languages using Bottom-up Tree Automata with Tree Pushdown Stores, J. Computer Science, (1985)
Partial Algebras for Representing Semantics of Information Systems Bericht Nr. 76 Kupka Hamburg IFI-HH-B-76/80
Pascal*: a Pascal Based Systems Programming Language Henessey TR 174 CSL Stanford Electronics Lab.
Passes, Sweeps an Visits in Attribute Grammars

Technische Hogeschool Twente INF-82-6; Engelfriet

Piton: A Verified Assembly Level Language Moore, CLI TR 22 1988
Problematic Features of PRogramming Languages: A situational-Calculus Approach. Pt 1 : Assignment Statements Manna, SRI TEchnical Note 226 1980
Process Handling on burroughs B6500 CLEARY, J. G. (1969): "Process Handling on Burroughs B6500" Proceedings of Fourth Australian Computer Conference, Adelaide, South Australia, August, 1969
Program proving as hand simulation with a little induction Rod M. Burstall. Program Proving as Hand Simulation with a Little Induction. In Proceedings of IFIP Congress'1974. pp.308~312 
Programming Languages: Linguistics & Semantics Dines Bjorner, Doc ID 672
Program Verification in the 1980's Problems, Perspectives, and Opportunities Gerhart ISI RR-78-71 1978
Propositional Dynamic Logic
Prototype Construction of a Compiler for Network Analysis Feasibility Study D.F. Martin, L.P. Laramie, R. Chen, D. Patterson. UCLA-ENG-7041 - sent to SRLF. online.
Proving Programs Incorrect Brand TR 99, 1976 U Toronto
Proving the Correctness of Digital Hardware Designs
Prudent Engineering Practice for Cryptographic Protocols SRC Research Report 125; Abadi
psfig/Tex 1.1 Users guide
Reasoning in Interval Temporal Logic
Revised (4) Report on the Algorithmic Language Scheme Link is to revision 5
SDVS 1987 Final Report The Aerospace Corporation ATR-86A(2778)-5. Not on Google.
Semantic Database Models King TR-101 1981 CS USC
Semantics and Pragmatics of the Lambda Calculus Wadsworth PHD thesis U Oxford
Sequential Circuit Verification using symbolic model checking
Some Fundamental properties of algebraic theories:  A tool for Semantics of Computation
Some Ideas on Algebraic Semantics Goguen UCLA and Third IBM Symposium on Mathematical foundations of Computer Science
Some Useful Modula-3 Interfaces SRC Research Report 113; Horning
Stack continuations: wandian semantics no sign in google
Standardization and Quantification of Computer Programs for Circuit Design D.F. Martin, L.P. McNamee, D.E. Meyerhoff, T.S. Chow - UCLA-ENG-7087 - Sent to SRLF  - not in Worldcat yet. No sign in google.
State-machine denotational semantics preliminary draft no sign in google
State-machine denotational semantics supplement 18 no sign in google
State-machine denotational semantics supplement 2 no sign in google
Strong Typing of Object-Oriented Languages Revisited Aarhaus DAIMI-PB-326; Madsen
Structure of a Portable Operating System Mendell TR CSRG-152 U Toronto
Summary of Changes Made to the Diana Reference Manual
Symbolic model checking with partitioned transition relations
Syntax directed translation of old programs into ADA no sign in google
Synthesis of Communicating processes from temporal logic specifications
Termination of Nondeterministic Programs De Bakker MAthematisch Centrum IW 50/75 Afdeling Informatica
The Automatic Assignment and Sequencing of Computations on Parallel Processor Systems D.F. Martin - Dissertation and UCLA Department of Engineering Report 66-4, 1966 - keeping in box, can't send to SRLF because I am afraid it might get tossed.  Title duplicates.
The 1993 SRC Algortithm Animation Festival SRC Research Report 126; Brown
The Algol '68 System at UCLA USE of SLR(1) Parsing Methods Farber UCLA Mod. and Meas. no 8
The AVA Reference Manual: Derived from ANSO/MIL-STD-1815A-1983 Modifications by Michael smith CLI TR 64 1992
The Birkoff Variety Theorem for Continuous Algebras
The Chemical Abstract Machine Berry INRIA 1133 1989 and POPL 90:81
The Contour Model of Block Structured Processes Johnston, GE 70-C-336 1970
The Correctness of a Precedence Parsing Algorithm on LCF Cohn University of Cambridge TR-21
The Correctness of a Simple Silicon Compiler Milne, G., The correctness of a simple silicon compiler. In: Proc. 6th Internat. Symp. on Computer Hardware Description Languages and their Applications, North-Holland, Amsterdam.
The Design and Verification of finite State Hardware Controllers Clarke, E., Bose, S., Browne, M, and Grumberg, O., The Design and Verification of Finite State Hardware Controllers. In: CS Dept Technical Report CMU-CS-87-145, Carnegie Mellon University.
The Formal Semantics of Computer Languages and their Implimentations. PhD, Univ Cambridge. 1974. Online. Discarded.
The J-machine : a fine grain concurrent computer In Proceedings of the IFIP (International Federation for Information Processing), 11th World Congress
The J-Machine system support for actors
The Lattice of Flow Diagrams
The ML Handbook Version 6.1  
The Specification and Application to Programming of Abstract Data Types Guttag CSRG-59 1975 U Toronto
The Taming of the Pointer Dembinski STC-2 CLG-139 1975 UCLA also ACM Sigplan notices 12(7):60
The Y Compiler Hanson TR-83-1 U Arizona
TLA in Pictures SRC Research Report 127; Lamport
Toward Interactive Design of Correct Programs Floyd, Stanford Artificial Intelligence Project AIM-150 and CS-235
Towards a Domain Theory for Termination Proofs
Towards Verified Systems Overview
Translation of Attribute Grammar into Procedures Katayama Tokyo Inst of Technology CS-K8001
Treatment of Ada Procedures: Aliasing, anomalies and Erroneousness BERRY, D.M. 1988. Treatment of Ada procedures: Aliasing, anomalies, and erroneousness. Tech. Rep., Unisys Corp., Santa Monica, Calif. Feb.
Two characterizations of partial and mixed computation no sign in google
Two Papers on Algebraic Data Type Implementation and Specification #109 Dortmund; Ehrich
Type Algebras. Functor Categories and Block Structure Aarhus DAIMI PB-156; Oles
Type Substitution for Object-Oriented Programming Aarhus DAIMI PB-317; PAlsberg
UBC Estelle - C Compiler (version 2.3) User's Manual and Internal Guide Vuong TR 90-2 UBC
UC a Language for the Connection Machine
Unified Algebras and Action Semantics Aarhus DAIMI PB-272; Mosses
Universal mechanisms for concurrency
Using domain algebras to prove the correctness of a compiler
Using HOL inside EMACS Windley, 1990 - U. Idaho TR CS-90-01
Using Rewriting Techniques to Produce Code-Generators and Proving them Correct Despland 1989 INRIA no 1046 and Science of Computer Programming 15(1):15
Verification of Arithmetic Circuits with Binary Moment Diagrams
Verification of Concurrent systems: function and Timing in ISBN:0-444-86481-4
Verification of futurebus cache coherence protocol Or at Springerlink
Verification of Programs Operating on Structured Data Laventhal, MIT TR-124
Verification tools for finite state concurrent systems
When are Two effectively given domains identical
Z and hol
Last modified: 7/9/2012 12:57 PM by M. Potter

General Campus Information

University of California, Riverside
900 University Ave.
Riverside, CA 92521
Tel: (951) 827-1012
UCR Career Opportunities
Library Job Opportunities

UCR Libraries Information

Directions / Mailing Addresses
Tomás Rivera Library: (951) 827-3220
Orbach Science Library: (951) 827-3701
Music Library: (951) 827- 3137
Multimedia Library: (951) 827-5606
UCR Libraries Visitor Guide

Related Links


UCR Libraries Facebook UCR Libraries Twitter UCR Libraries YouTube UCR Libraries News UCR Libraries Mobile Website