Search results for "soundness"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
7	David M. Goldschlag	Mechanically Verifying Concurrent Programs with the Boyer-Moore Prover.	IEEE Trans. Software Eng.	1990	DBLP DOI BibTeX RDF	mechanically verifying concurrent programs, Boyer-Moore prover, transition system model, parallel programming, distributed algorithm, concurrency, theorem proving, program verification, safety, encoding, encoding, operational semantics, inference mechanisms, liveness, inference rules, proof system, Unity
7	Julian C. Bradfield	Proving temporal properties of Petri Nets.	Applications and Theory of Petri Nets	1990	DBLP DOI BibTeX RDF	model-checking, Petri nets, temporal logic, tableau systems
7	John C. Mitchell	Toward a Typed Foundation for Method Specialization and Inheritance.	POPL	1990	DBLP DOI BibTeX RDF
7	Wayne Snyder	Higher Order E-Unification.	CADE	1990	DBLP DOI BibTeX RDF
7	Uwe Petermann	Towards a Connection Procedure with Built in Theories.	JELIA	1990	DBLP DOI BibTeX RDF
7	Alan M. Frisch, Richard B. Scherl	A Constraint Logic Approach to Modal Deduction.	JELIA	1990	DBLP DOI BibTeX RDF
7	Mark E. Stickel	A Prolog Technology Theorem Prover: A New Exposition and Implementation in Prolog.	DISCO	1990	DBLP DOI BibTeX RDF
7	Yiannis N. Moschovakis	A Mathematical Modeling of Pure, Recursive Algorithms.	Logic at Botik	1989	DBLP DOI BibTeX RDF
7	Martín Abadi, Luca Cardelli, Benjamin C. Pierce, Gordon D. Plotkin	Dynamic Typing in a Statically-Typed Language. (long version: TOPLAS 13 (2): 237-268 (1991))	POPL	1989	DBLP DOI BibTeX RDF
7	Sanjay Manchanda	Declarative Expression of Deductive Database Updates.	PODS	1989	DBLP DOI BibTeX RDF	Prolog
7	Pierre Jouvelot, David K. Gifford	Reasoning about Continuations with Control Effects.	PLDI	1989	DBLP DOI BibTeX RDF
7	Milind Gandhe, G. Venkatesh	Improving Prolog Performance by Inductive Proof Generalizations.	KBCS	1989	DBLP DOI BibTeX RDF
7	Bharat Jayaraman	Semantics of EqL.	IEEE Trans. Software Eng.	1988	DBLP DOI BibTeX RDF	Correctness theorems, equational programming, equation solving, object refinement, logic programming, functional programming, denotational semantics, reduction semantics
7	John M. Lucassen, David K. Gifford	Polymorphic Effect Systems.	POPL	1988	DBLP DOI BibTeX RDF
7	Saumya K. Debray	Efficient Dataflow Analysis of Logic Programs.	POPL	1988	DBLP DOI BibTeX RDF
7	W. P. Weijland	Semantics for Logic Programs without Occur Check.	ICALP	1988	DBLP DOI BibTeX RDF
7	Gary S. Delp, Adarshpal S. Sethi, David J. Farber	An analysis of Memnet - an experiment in high-speed shared-memory local networking.	SIGCOMM	1988	DBLP DOI BibTeX RDF
7	Philippe le Chenadec	On Positive Occur-Checks in Unification.	MFCS	1988	DBLP DOI BibTeX RDF
7	Tie-Cheng Wang	Elements of Z-Module Reasoning.	CADE	1988	DBLP DOI BibTeX RDF
7	Andrei Voronkov	A proof-search method for the first-order logic.	Conference on Computer Logic	1988	DBLP DOI BibTeX RDF
7	Anne Neirynck, Prakash Panangaden, Alan J. Demers	Computation of Aliases and Support Sets.	POPL	1987	DBLP DOI BibTeX RDF
7	Joylyn Reed	Semantics-Based Tools for a Specification-Support Environment.	MFPS	1987	DBLP DOI BibTeX RDF
7	Hendrik Pieter Barendregt, Marko C. J. D. van Eekelen, John R. W. Glauert, Richard Kennaway, Marinus J. Plasmeijer, M. Ronan Sleep	Term Graph Rewriting.	PARLE (2)	1987	DBLP DOI BibTeX RDF
7	Kesav V. Nori, Sanjeev Kumar, M. Pavan Kumar	Retrospection on the Compiler Structure.	FSTTCS	1987	DBLP DOI BibTeX RDF
7	Krzysztof R. Apt, Gordon D. Plotkin	Countable nondeterminism and random assignment.	J. ACM	1986	DBLP DOI BibTeX RDF
7	Dennis de Champeaux	Subproblem finder and instance checker, two cooperating modules for theorem provers.	J. ACM	1986	DBLP DOI BibTeX RDF
7	Raymond Reiter	A sound and sometimes complete query evaluation algorithm for relational databases with null values.	J. ACM	1986	DBLP DOI BibTeX RDF
7	Harald Søndergaard	An Application of Abstract Interpretation of Logic Programs: Occur Check Reduction.	ESOP	1986	DBLP DOI BibTeX RDF
7	Mark E. Stickel	A prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler.	CADE	1986	DBLP DOI BibTeX RDF
7	Philip T. Cox, Tomasz Pietrzykowski	Causes for Events: Their Computation and Applications.	CADE	1986	DBLP DOI BibTeX RDF
7	Jonathan Traugott	Nested Resolution.	CADE	1986	DBLP DOI BibTeX RDF
7	Barry Burd	Using subprograms as the main primitive in teaching Ada (abstract only).	ACM Conference on Computer Science	1985	DBLP DOI BibTeX RDF
7	Joseph Y. Halpern, John H. Williams, Edward L. Wimmers, Timothy C. Winkler	Denotational Semantics and Rewrite Rules for FP.	POPL	1985	DBLP DOI BibTeX RDF	FP
7	Satoru Tomura	TDProlog: An Extended Prolog with Term Description.	LP	1985	DBLP DOI BibTeX RDF
7	John McLean	A Formal Method for the Abstract Specification of Software.	J. ACM	1984	DBLP DOI BibTeX RDF
7	Hiroyuki Izumi, Yasuyoshi Inagaki, Namio Honda	A Complete Axiom System for Algebra of Closed-Regular Expression.	ICALP	1984	DBLP DOI BibTeX RDF
7	Mario Coppo, Elio Giovannetti	Completeness Results for a Polymorphic Type System.	CAAP	1983	DBLP DOI BibTeX RDF
7	Krzysztof R. Apt, Gordon D. Plotkin	A Cook's Tour of Countable Nondeterminism.	ICALP	1981	DBLP DOI BibTeX RDF
7	Philip T. Cox, Tomasz Pietrzykowski	A Complete, Nonredundant Algorithm for Reversed Skolemization.	CADE	1980	DBLP DOI BibTeX RDF
7	Patricia P. Griffiths, Charles J. Prenner	Verifying Formal Specifications of Synchronous Processes.	POPL	1976	DBLP DOI BibTeX RDF
7	Marco Colombetti, Enrico Pagello	Programs, Computations and Temporal Features.	MFCS	1976	DBLP DOI BibTeX RDF	Predicate-Logic-like Programming Language, Control Structures Temporal Features, Restrictions