%T The Theory of Joins in Relational Databases
%J Proc. 18th IEEE Symp. on Foundations of Computer Science
%T Equivalence of Relational Expressions
%T Dependency Structures of Data Base Relationships
%T An Algorithmic Approach to Normalization of Relational Database Schemes
%I Computer Science Research Group, University of Toronto
%T A Complete Axiomatization for Functional and Multivalued Dependencies
%I IBM, San Jose, California
%T Optimal Implementation of Conjunctive Queries in Relational Data Bases
%J Proc. 9th ACM Symp. on Theory of Computing
%T A Relational Model for Large Shared Data Bases
%J Comm. Assoc. Comp. Mach.
%T Further Normalization of the Data Base Relational Model
%C Englewood Cliffs, N. J
%T Relational Completeness of Data Base Sublanguages
%C Englewood Cliffs, N. J
%T The Complexity of Theorem Proving Procedures
%J Proc. 3rd ACM Symp. on Theory of Computing
%T An Introduction to Database Systems
%T Contributions Theoretiques a la Conception d'un Systeme d'informations
%O Ph. D. thesis, Univ. of Grenoble, Oct
%T Multivalued Dependencies and a New Normal Form for Relational Databases
%J ACM Trans. Data Base Systems
%T Optimization of a Single Relational Expression in a Relational
%J IBM J. Research and Development
%T Reducibility Among Combinatorial Problems
%B Complexity of Computer Computations
%E R. E. Miller and J. W. Thatcher
%T Candidate Keys for Relations
%O (To appear; available from Department of Computer Science, University of Waterloo).
%T Performing Inferences over Relational Databases
%R TR363, Department of Computer Science
%I University of Maryland
%T Efficient Evaluation of Expressions in a Relational Algebra
%J Proc. ACM Pacific Conf.
%T A Database Search Problem
%B Information Systems COINS IV
%T Independent Components of Relations
%R RJ1899, IBM, San Jose, California
%T Optimizing the Performance of a Relational Algebra Database Interface
%J Comm. Assoc. Comp. Mach.
%T Observations on Data Manipulation Languages and their
Embedding in General Purpose Programming Languages
%I University of California, Berkeley
%T Decomposition \(em a Strategy for Query Processing
%J ACM Trans. Data Base Systems
%T Analysis and Design of Relational Schemata for Database Systems
%R Tech. Rept. UCLA-ENG-7769
%I Department of Computer Science, UCLA
%T Query-by-Example: the Invocation and Definition of Tables and Forms
%J Proc. ACM International Conf. on Very Large Data Bases
%T A lambda calculus model of programming languages \(em I. simple constructs
%T A lambda calculus model of programming languages \(em II. jumps and procedures
%A ADJ (J. A. Goguen, J. W. Thatcher, E. G. Wagner and J. B Wright)
%T A junction between category theory and computer science, I: basic concepts and examples (Part 1)
%C Yorktown Heights, N. Y.
%A ADJ (J. A. Goguen, J. W. Thatcher, E. G. Wagner and J. B Wright)
%T A junction between category theory and computer science, I: basic concepts and examples (Part 2)
%C Yorktown Heights, N. Y.
%T How program statements transform predicates
%T On forward and backward proof rules for program verification
%T Semanol (73) A metalanguage for programming the semantics of programming languages
%T Equivalence of operational and denotational semantics for a fragment of Pascal
%T Exercises in denotational semantics
%J Lecture Notes in Computer Science
%T Semantics and proof theory of Pascal procedures
%J Lecture Notes in Computer Science
%T Completeness with finite systems of intermediate assertions for recursive program schemas
%T Non deterministic recursive program schemes
%T On nondeterministic program schemes
%T Remarks on ``Program proving: jumps and functions by M. Clint and C. A. R. Hoare''
%T The Fortran automatic coding system
%J Western Computer Proceedings
%T Producing optimised code for coercions
%J Information Processing Letters
%T A global representation of the recursive functions in the $lambda -$claculus
%T Towards a mathematical theory of processes
%T Bottom-up computation of recursive programs
%R Rapport de Recherche No 133
%T Program equivalence and canonical forms in stable discrete interpretations
%E S. Michaelson and R. Milner
%B Automata Languages and Programming , Third International Colloquium
%I Edinburgh University Press
%T Minimal and optimal computations of recursive programs
%T Programs with subscripted variables
%J Bulletin de L'Academie Polonaise des Sciences, Serie des sciences math., astr. et phys.
%T The CUCH as a formal and description language
%B Formal language description languages for computer programming
%T Extended type checking
%T Algol 68C Reference Manual
%I Computer Laboratory, Cambridge University
%T A computer proof of the correctness of a simple optimizing compiler for expressions
%T An algorithmic semantics for Algol 60 identifier denotation
%T Semantics of assignment
%E Ella Dale and Donald Michie
%B Machine Intelligence 2
%T Proving properties of programs by structural induction
%T Some techniques for proving properties of programs which alter data structures
%T Program invariants as fixed points
%J Proc. 18th IEEE Symp. on Foundations of Computer Science
%T Program proving: coroutines
%T Program proving:jumps and functions
%O see also Ashcroft, Clint and Hoare (1976)
%T Soundness and completeness of an axiom system for program verification
%T An assertion language for data structures
%J Proc. 2nd ACM Symp. on Principles of Programming Languages
%T Program scheme equivalences and second-order logic
%T On the definition of classes of interpretations
%R Rapport de Recherche No 231
%T On some classes of interpretations
%R Rapport de Recherche No 253
%T Completeness results for the equivalence of recursive schema
%T A model for the formal definition of programming languages
%T A note on the semantic definition of side effects
%J Information Processing Letters
%T Simula 67: common base language
%I Norwegian Computing Centre
%T Semantics of programming languages
%B Advances in Information Systems Science, Vol. 2
%I Mathem
\ 1atical Centre Tracts 24, Mathematisch Centrum
%T Recursion, induction and symbol manipulation
%B Informatica Symposium 1971
%I Mathematisch Centre Tracts 25, Mathematisch Centrum
%T Axiom systems for simple assignment statements
%J Lecture Notes in Mathematics
%T A property of linear conditionals
%J Lecture Notes in Mathematics
%T The fixpoint approach in semantics: theory and applications
%B Foundations of Computer Science
%I Mathematical Centre Tracts 63
%T Least fixed points revisited
%T Fixed point semantics and Dijkstra's fundamental invariance theorem
%T Correctness proofs for assignment statements
%T Semantics and the foundations of program proving
%B Information Processing 77
%T Recursive programs as predicate transformers
%B IFIP Working Conference on the Formal Description of Programming Concepts
%T On the completeness of the inductive assertion method
%A Mariangiola Dezani-Ciancaglini
%T Application of Church-Rosser properties to increase the parallelism and efficiency of algorithms
%J Lecture Notes in Computer Science
%T A Discipline of Programming
%C Englewood Cliffs, N. J.
%T The mathematical semantics of axiomatically defined programming language constructs
%B Proving and Improving Programs
%T Complementary Definitions of Programming Language Semantics
%J Lecture Notes in Computer Science
%T Locations considered unnecessary
%T A mathematical model for non-deterministic computations
%T Computability concepts for programming language semantics
%T Rules of inference for procedure calls
%T Assigning meanings to programs
%B Mathematical Aspects of Computer Science, Proceedings of a Symposium in Applied Mathematics, Vol. 19
%T Backtracking in recursive computations
%T The definition of programming languages by their compilers
%B Formal Language Description Languages for Computer Programming
%T Operational reasoning and denotational semantics
%B Proving and Improving Programs
%T A complete axiomatic system for proving assertions about recursive and nonrecursive programs
%I Department of Computer Science, University of Toronto
%T Assignment to subscripted variables
%I Department of Computer Science, Cornell University
%T An illustration of current ideas on the derivation of correctness proofs and correct programs
%J IEEE Trans. on Software Engineering
%T Some ideas on data types in high level languages
%J Comm. Assoc. Comp. Mach.
%T Semantic equivalence of program schemes and its syntactic characterization
%E S. Michaelson and R. Milner
%B Automata, Languages and Programming, Third International Colloquium
%I Edinburgh University Press
%T Sur quelques applications de la semantique algebrique des schemas recursifs polyadiques
%T Abstract data types and the development of data structures
%J Comm. Assoc. Comp. Mach.
%T Abstract data types and software validation
%I Information Sciences Institute, University of Southern California
%T The design of data type specifications
%I Information Sciences Institute, Univeristy of Southern California
%T Arithmetical completeness in logics of programs
%T On the correctness of regular deterministic programs; a unifying survey
%T Complete axiomatization of properties of recursive programs (extended abstract)
%T A complete axiomatic system for proving deductions about recursive programs
%J Ninth ACM Symp. Theory of Computing
%T Nondeterminism in logics of programs
%J Proc. 5th ACM Symp. on Principles of Programming Languages
%T Formal semantics of a schematic intermediate language
%C Yorktown Heights, N. Y.
%T Efficient implementation of a class of recursively defined functions
%J Proc. 3rd ACM Symp. on Principles of Programming Languages
%T Parameter passing mechanisms and non-determinism
%T The semantics of nondeterminism
%I Department of Computer Science, University of Waterloo
%T An axiomatic basis for computer programming
%J Comm. Assoc. Comp. Mach.
%T Procedures and parameters: an axiomatic approach
%J Lecture Notes in Mathematics
%T Proof of correctness of data representations
%T Hints on programming language design
%O Invited address at ACM Symposium on Principles of Programming Languages.
%T Some properties of non-deterministic computations
%T Consistent and complementary formal theories of the semantics of programming languages
%T Design and correctness of a compiler for Lucid
%R Research Report CS-76-20
%I Computer Science Department, University of Waterloo
%T A completeness theorem for straight-line programs with structured variables
%T The retracts in $P omega$ do not form a continuous lattice \(em a solution to Scott's problem
%T Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
%J Proc. 18th IEEE Symp. on Foundations of Computer Science
%T Program transformations in classes of interpretations
%T Semantics of Algol-like statements
%J Lecture Notes in Mathematics
%T Automatic program verification I: a logical basis and its implementation
%T An investigation into different semantic approaches
%I Department of Computer Science, University of Aarhus
%T An approach to systems correctness
%T The semantics of a simple language for parallel programming
%B Information Processing 74
%T Coroutines and networks of parallel processes
%B Information Processing 77
%T Some completeness results in the mathematical theory of computation
%T Denotational models for parallel programs with indeterminate operators
%B IFIP Working Conference on the Formal Description of Programming Concepts
%T Simple word problems in universal algebras
%B Computational Problems in Abstract Algebra
%T Early development of programming languages
%B Encyclopedia of Computer Science and Technology, Vol. 7
%T On the equivalence of modes and the equivalence of finite automata
%T The mechanical evaluation of expressions
%T A correspondence between Algol 60 and Church's lambda-notation
%J Comm. Assoc. Comp. Mach.
%D February and March 1965
%T A formal description of Algol 60
%B Formal Language Description Languages for Computer Programming
%T The next 700 programming languages
%J Comm. Assoc. Comp. Mach.
%T A $lambda -$calculus approach
%B Advances in Programming and Non-numerical Computation
%T On correct procedure parameter transmission in higher programming languages
%T On deciding word problems by rewrite rule simplifiers
%T A model for type checking \(em with an application to Algol 60
%J Comm. Assoc. Comp. Mach.
%T The formal definition of the Basic language
%J Proc. 18th IEEE Symp. on Foundations of Computer Science
%T Proof rules, mathematical semantics and programming language design
%T Surface properties of programming language constructs
%T A necessary and sufficient condition for the existence of Hoare logics
%J Proc. 18th IEEE Symp. on Foundations of Computer Science
%T A bibliography on proving the correctness of programs
%B Machine Intelligence 5
%I Edinburgh University Press, Edinburgh, and American Elsevier, New York, N. Y.
%T Abstraction and verification in Alphard: a symbol table example
%T On the semantics of programming languages and software devices
%B Formal Semantics of Programming Languages
%C Englewood Cliffs, N. J.
%T Formal definition of programming languages and systems
%B Information Processing 71
%T On the formal definition of PL/I
%J Annual Review of Automatic Programming
%T On formalized computer programs
%T Automatic program verification V: verification oriented proof rules for arrays, records and pointers
%T Proof of termination within a weak logic of programs
%T Extended data graphs, a formalism for structured data and data structures
%T Inductive methods for proving properties of programs
%J Comm. Assoc. Comp. Mach.
%T Fixpoint approach to the theory of computation
%J Comm. Assoc. Comp. Mach.
%T categories of chain-complete posets
%T Bases for chain-complete posets
%J IBM J. Research and Development
%T Induction principles for context-free languages
%J Lecture Notes in Computer Science
%T Recursive functions of symbolic expressions and their computation by machine, part I
%J Comm. Assoc. Comp. Mach.
%T Towards a mathematical science of computation
%B Information Processing 1962
%T A basis for a mathematical theory of computation
%E P. Braffort and D. Hirschberg
%B Computer Programming and Formal Systems
%T A formal description of a subset of Algol
%B Formal Language Description Languages for Computer Programming
%T Correctness of a compiler for arithmetic expressions
%B Proceedings of Symposia in Applied Mathematics, Volume XIX
%I American Math. Society
%T Verifying the correctness of implementations
%T Transforming predicate transformers
%B IFIP Working Conference on the Formal Description of Programming Concepts
%I Computer Science Department, Stanford University
%T Processes; a model of computing agents
%T Program semantics and mechanized proof
%I Mathematical Centre Tracts 82
%T LCF; a methodology for performing rigorous proofs about programs
%B First IBM Symposium on Mathematical Foundations of Computer Science
%I Academic and Scientific Programs, IBM Japan
%T Another recursion induction principle
%J Comm. Assoc. Comp. Mach.
%T The mathematical semantics of Algol 60
%R Technical Monograph PRG-12
%I Programming Research Group, Oxford University
%T The semantics of semantic equations
%J Lecture Notes in Computer Science
%T Compiler generation using denotational semantics
%J Lecture Notes in Computer Science
%T Making denotational semantics less concrete
%T On some families of languages related to the Dyck language
%J Proc. 2nd ACM Symp. on Theory of Computing
%T On the interpretation of recursive program schemes
%R Rapport de Recherche No 84
%T Subtree replacement systems: a unifying theory for recursive equations, Lisp, Lucid and combinatory logic
%J Ninth ACM Symp. Theory of Computing
%T Proving assertions about programs that manipulate data structures
%J Proc. 7th ACM Symp. on Theory of Computing
%T Programming language data structures: a comparative study
%I Department of Computer Science, Rutgers University
%T An optimal fix-point computation rule for a simple recursive language
%I Consiglio Nazionale delle Ricerche, Istituto di Elaborazione della Informazione
%T Graph representation and computation rules for typeless recursive languages
%J Lecture Notes in Computer Science
%T On interpreter oriented definitions of programming languages
%T Some semantics for data structures
%B Machine Intelligence 3
%T Fixpoint induction and proofs of program properties
%B Machine Intelligence 5
%T Finiteness is mu-ineffable
%T A family of rules for recursion removal
%J Information Processing Letters
%T A set-theoretical definition of application
%I School of Artificial Intelligence, University of Edinburgh
%T Lambda-definability and logical relations
%I School of Artificial Intelligence, University of Edinburgh
%T Call-by-name, call-by-value and the $lambda -$calculus
%T The temporal logic of programs
%J Proc. 18th IEEE Symp. on Foundations of Computer Science
%T Semantical considerations in Floyd-Hoare logic
%J Proc. 17th IEEE Symp. on Foundations of Computer Science
%T Operational and semantic equivalence between recursive programs
%T Relational and continuation semantics for a simple imperative language
%B Seminaires IRIA: theorie des algorithmes, des langages et de la programmation
%T On the relation between direct and continuation semantics
%J Lecture Notes in Computer Science
%O preliminary draft for Cosers
%T Semantics of the domain of flow diagrams
%T Recursion and iteration
%J Comm. Assoc. Comp. Mach.
%T Converting a class of recursive procedures into non-recursive ones
%J Software \(em Practice and Experience
%T Implementation correctness involving a language with goto statements
%T On an equivalence between continuation and stack semantics
%T Procedures, formal computations and models
%J Lecture Notes in Computer Science
%T The lambda calculus, lattice theory and reflexive domains
%T Computability theory in admissible domains
%T Outline of a mathematical theory of computation
%J Proc. 4th Princeton Conf. on Information Sciences and Systems
%T The lattice of flow diagrams
%J Lecture Notes in Mathematics
%B Toposes, Algebraic Geometry and Logic
%I Lecture Notes in Mathematics 274, Springer Verlag
%T Mathematical concepts in programming language semantics
%T A simplified construction for $lambda -$calculus models
%T Data types as lattices
%T Logic and programming languages
%J Comm. Assoc. Comp. Mach.
%T Towards a mathematical semantics for computer languages
%B Proceedings of the Symposium on Computers and Automata
%J Lecture Notes in Computer Science
%T Abstraction and verification in Alphard: iteration and generators
%I Information Sciences Institute, University of Southern California
%T The category-theoretic solution of recursive domain equations
%J Proc. 18th IEEE Symp. on Foundations of Computer Science
%T The congruence of two programming language definitions
%T Towards a formal semantics
%B Formal Language Description Languages for Computer Programming
%T Varieties of programming language
%B International Computing Symposium Proceedings
%T Continuations: a mathematical semantics which can deal with full jumps
%R Technical Monograph PRG-11
%I Programming Research Group, Oxford University
%T Chain properties in P$omega$
%T A lattice-theoretical fixpoint theorem and its applications
%T Mathematical semantics of Snobol 4
%J Proc. ACM Symp. on Principles of Programming Languages
%T The denotational semantics of programming languages
%J Comm. Assoc. Comp. Mach.
%T Language design methods based on semantic principles
%T A denotational definition of the programming language Pascal
%I Department of Computing and Information Science, Queen's University
%T Recursive definition of syntax and semantics
%B Formal Language Description Languages for Computer Programming
%T Characterizations of flowchartable recursions
%T A characterization of weakest preconditions
%T Procedure closure in EL1
%T The treatment of data types in EL1
%J Comm. Assoc. Comp. Mach.
%T Constructive methods in program verification
%J IEEE Trans. on Software Engineering
%T An introduction to the construction and verification of Alphard programs
%J IEEE Trans. on Software Engineering