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 : http://ftp.funet.fi/index/languages/ml/cml/CMLDOC-0.9.6.ps.Z |
| 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 |
| 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
