Search results for "soundness"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
7	Yohji Akama	SN Combinators and Partial Combinatory Algebras.	RTA	1998	DBLP DOI BibTeX RDF
7	Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani, Serdar Tasiran	An Assume-Guarantee Rule for Checking Simulation.	FMCAD	1998	DBLP DOI BibTeX RDF
7	Ken-etsu Fujita	Polymorphic Call-by-Value Calculus Based on Classical Proofs.	AISC	1998	DBLP DOI BibTeX RDF
7	Nicolette Bonnette, Rajeev Goré	A Labelled Sequent System for Tense Logic Kt.	Australian Joint Conference on Artificial Intelligence	1998	DBLP DOI BibTeX RDF	labelled deductive system, lean deduction, sequent system, automated deduction, tense logic
7	A. Prasad Sistla	Parametrized Verification of Linear Networks Using Automata as Invariants.	CAV	1997	DBLP DOI BibTeX RDF
7	María Alpuente, Moreno Falaschi, Pascual Julián Iranzo, Germán Vidal	Specialization of Lazy Functional Logic Programs.	PEPM	1997	DBLP DOI BibTeX RDF	integration of functional and logic programming, lazy narrowing, post-processing renaming, partial evaluation, term rewriting systems
7	Jesús Manuel Almendros-Jiménez, Ana Gil-Luezas	Lazy Narrowing with Parametric Order Sorted Types.	ALP/HOA	1997	DBLP DOI BibTeX RDF
7	Makoto Tanabe	Timed Petri Nets and Temporal Linear Logic.	ICATPN	1997	DBLP DOI BibTeX RDF	temporal linear logic, timed Petri nets, quantales
7	Kan Zhang	A Theory for System Security.	CSFW	1997	DBLP DOI BibTeX RDF
7	Judicaël Courant	An Applicative Module Calculus.	TAPSOFT	1997	DBLP DOI BibTeX RDF
7	Puri Arenas-Sánchez, Mario Rodríguez-Artalejo	A Semantic Framework for Functional Logic Programming with Algebraic Polymorphic Types.	TAPSOFT	1997	DBLP DOI BibTeX RDF
7	Martín Abadi, K. Rustan M. Leino	A Logic of Object-Oriented Programs.	TAPSOFT	1997	DBLP DOI BibTeX RDF
7	Mihir Bellare, Russell Impagliazzo, Moni Naor	Does Parallel Repetition Lower the Error in Computationally Sound Protocols?	FOCS	1997	DBLP DOI BibTeX RDF
7	Sophia Drossopoulou, Susan Eisenbach	Java is Type Safe - Probably.	ECOOP	1997	DBLP DOI BibTeX RDF
7	Bernd Fischer 0002, Johann Schumann	SETHEO Goes Software Engineering: Application of ATP to Software Reuse.	CADE	1997	DBLP DOI BibTeX RDF
7	Tom Cornell	Derivational and Representational Views of Minimalist Tranformational Grammar.	LACL	1997	DBLP DOI BibTeX RDF
7	Donald Nute, Christopher Henderson, Zachary Hunter	d-Graph: An Argument-Based System Incorporating Defensible Graphs.	HICSS (5)	1997	DBLP DOI BibTeX RDF
7	Eiichiro Fujisaki, Tatsuaki Okamoto	Statistical Zero Knowledge Protocols to Prove Modular Polynomial Relations.	CRYPTO	1997	DBLP DOI BibTeX RDF
7	Robert Glück, Jesper Jørgensen	Fast Binding-Time Analysis for Multi-Level Specialization.	Ershov Memorial Conference	1996	DBLP DOI BibTeX RDF	generating extensions, program transformation, program analysis, partial evaluation, functional languages
7	C. Norris Ip, David L. Dill	Verifying Systems with Replicated Components in Murphi.	CAV	1996	DBLP DOI BibTeX RDF
7	Andrei Kovalyov	An O(\|S\|×\|T\|)- Algorithm to Verify if a Net is Regular.	Application and Theory of Petri Nets	1996	DBLP DOI BibTeX RDF
7	Peter J. Stuckey, Vincent W. L. Tam	Models for Using Stochastic Constraint Solvers in Constraint Logic Programming.	PLILP	1996	DBLP DOI BibTeX RDF
7	Nicola Leone, Pasquale Rullo, Francesco Scarcello	On the Computation of Disjunctive Stable Models.	DEXA	1996	DBLP DOI BibTeX RDF
7	Geoffrey Smith 0001, Dennis M. Volpano	Towards an ML-Style Polymorphic Type System for C.	ESOP	1996	DBLP DOI BibTeX RDF
7	Fabien Coelho	Discussing HPF Design Issues.	Euro-Par, Vol. I	1996	DBLP DOI BibTeX RDF
7	Maria Paola Bonacina, Jieh Hsiang	On Semantic Resolution with Lemmaizing and Contraction.	PRICAI	1996	DBLP DOI BibTeX RDF
7	Thomas Kolbe, Christoph Walther	Termination of Theorem Proving by Reuse.	CADE	1996	DBLP DOI BibTeX RDF
7	Thomas Arts	Termination by Absence of Infinite Chains of Dependency Pairs.	CAAP	1996	DBLP DOI BibTeX RDF
7	Paolo Di Blasio, Kathleen Fisher	A Calculus for Concurrent Objects.	CONCUR	1996	DBLP DOI BibTeX RDF
7	Maria C. F. Ferreira	Dummy Elimination in Equational Rewriting.	RTA	1996	DBLP DOI BibTeX RDF
7	Herman Geuvers	Extending Models of Second Order Predicate Logic to Models of Second Dependent Type Theory.	CSL	1996	DBLP DOI BibTeX RDF
7	Tobias Nipkow	Winskel is (Almost) Right: Towards a Mechanized Semantics Textbook.	FSTTCS	1996	DBLP DOI BibTeX RDF
7	Paolo Ciancarini, Daniela Fogli, Mauro Gaspari	A Logic Language based on GAMMA-like Multiset Rewriting.	ELP	1996	DBLP DOI BibTeX RDF
7	Anatoli Degtyarev, Andrei Voronkov	Handling Equality in Logic Programming via Basic Folding.	ELP	1996	DBLP DOI BibTeX RDF
7	Jens Palsberg, Cun Xiao, Karl J. Lieberherr	Efficient Implementation of Adaptive Software.	ACM Trans. Program. Lang. Syst.	1995	DBLP DOI BibTeX RDF	object traversal, correctness proof, adaptive software
7	Divesh Srivastava, S. Sudarshan 0001, Raghu Ramakrishnan 0001, Jeffrey F. Naughton	Space Optimization in Deductive Databases.	ACM Trans. Database Syst.	1995	DBLP DOI BibTeX RDF	bottom-up query evaluation deductive database systems, discarding facts, logic programming
7	Weidong Chen	Query Evaluation in Deductive Databases with Alternating Fixpoint Semantics	ACM Trans. Database Syst.	1995	DBLP DOI BibTeX RDF	alternating fixpoint, deductive databases, query evaluations, negation, predicate logic, SLG resolution
7	Patrick Cousot, Radhia Cousot	Compositional and Inductive Semantic Definitions in Fixpoint, Equational, Constraint, Closure-condition, Rule-based and Game-Theoretic Form.	CAV	1995	DBLP DOI BibTeX RDF
7	Otmane Aït Mohamed	Mechanizing a pi-Calculus Equivalence in HOL.	TPHOLs	1995	DBLP DOI BibTeX RDF
7	Bernd Bütow, Robert Giegerich, Enno Ohlebusch, Stephan Thesing	A New Strategy for Semantic Matching	PLILP	1995	DBLP DOI BibTeX RDF
7	Huimin Lin	Complete Inference Systems for Weak Bisimulation Equivalences in the pi-Calculus.	TAPSOFT	1995	DBLP DOI BibTeX RDF
7	Hanne Riis Nielson, Flemming Nielson	Static and Dynamic Processor Allocation for Higher-Order Concurrent Languages.	TAPSOFT	1995	DBLP DOI BibTeX RDF
7	Volker Diekert, Paul Gastin	A Domain for Concurrent Termination: A Generalization of Mazurkiewicz Traces (Extended Abstract).	ICALP	1995	DBLP DOI BibTeX RDF
7	Milena Stefanova, Herman Geuvers	A Simple Model Construction for the Calculus of Constructions.	TYPES	1995	DBLP DOI BibTeX RDF
7	Pierre-Yves Calland, Tanguy Risset	Precise Tiling for Uniform Loop Nests.	ASAP	1995	DBLP DOI BibTeX RDF	uniform dependence algorithm, convex cone, partitionning, tiling, loop nest
7	Robert Pearson	Linking fabrication and parametric testing to VLSI design courses.	Great Lakes Symposium on VLSI	1995	DBLP DOI BibTeX RDF	VLSI design courses, simulation model parameters, VLSI, integrated circuit testing, integrated circuit design, integrated circuit modelling, educational courses, device models, parametric testing, electronic engineering education
7	Till Mossakowski	Equivalences among Various Logical Frameworks of Partial Algebras.	CSL	1995	DBLP DOI BibTeX RDF
7	Lunjin Lu	A Generic Declarative Diagnoser for Normal Logic Programs.	LPAR	1994	DBLP DOI BibTeX RDF
7	Donald A. Smith, Timothy J. Hickey	Multi-SLD Resolution.	LPAR	1994	DBLP DOI BibTeX RDF
7	Neil D. Jones, Mads Rosendahl	Higher-Order Minimal Functional Graphs.	ALP	1994	DBLP DOI BibTeX RDF
7	Brian T. Graham	An Interpretation of NODEN in HOL.	TPHOLs	1994	DBLP DOI BibTeX RDF
7	Peter V. Homeier, David F. Martin	Trustworthy Tools for Trustworthy Programs: A Verified Verification Condition Generator.	TPHOLs	1994	DBLP DOI BibTeX RDF
7	Frank S. de Boer, Maurizio Gabbrielli, Elena Marchiori, Catuscia Palamidessi	Proving Concurrent Constraint Programs Correct.	POPL	1994	DBLP DOI BibTeX RDF
7	Satish R. Thatte	Semantics of Type Classes Revisited.	LISP and Functional Programming	1994	DBLP DOI BibTeX RDF	Haskell
7	Zhong Shao, John H. Reppy, Andrew W. Appel	Unrolling Lists.	LISP and Functional Programming	1994	DBLP DOI BibTeX RDF
7	Andy Mück, Thomas Streicher	A Tiny Constrain Functional Logic Language and Its Continuation Semantics.	ESOP	1994	DBLP DOI BibTeX RDF
7	James H. Andrews	Foundational Issues in Implementing Constraint Logic Programming Systems.	ESOP	1994	DBLP DOI BibTeX RDF
7	Michael Hanus	Lazy Unification with Simplification.	ESOP	1994	DBLP DOI BibTeX RDF
7	Bernhard Beckert	A Completion-Based Method for Mixed Universal and Rigid E-Unification.	CADE	1994	DBLP DOI BibTeX RDF
7	Martin Protzen	Lazy Generation of Induction Hypotheses.	CADE	1994	DBLP DOI BibTeX RDF
7	Jean-Pierre Banâtre, Ciarán Bryce, Daniel Le Métayer	Compile-Time Detection of Information Flow in Sequential Programs.	ESORICS	1994	DBLP DOI BibTeX RDF	formal verification, program analysis, computer security, information flow, verification tools
7	Viviana Bono, Luigi Liquori	A Subtyping for the Fisher-Honsell-Mitchell Lambda Calculus of Objects.	CSL	1994	DBLP DOI BibTeX RDF
7	Matt Fairtlough, Michael Mendler	An Intuitionistic Modal Logic with Applications to the Formal Verification of Hardware.	CSL	1994	DBLP DOI BibTeX RDF
7	Matthias Baaz, Gernot Salzer	Semi-Unification and Generalizations of a Particularly Simple Form.	CSL	1994	DBLP DOI BibTeX RDF
7	A. Udaya Shankar	An Introduction to Assertional Reasoning for Concurrent Systems.	ACM Comput. Surv.	1993	DBLP DOI BibTeX RDF	generation of preconditions, leads-to, progress properties, invariants, Hoare logic, weakest preconditions, safety properties, state transition systems, assertional reasoning
7	Hiu Fai Chau	A Proof Search System for a Modal Substructural Logic Based on Labelled Deductive Systems.	LPAR	1993	DBLP DOI BibTeX RDF
7	Reiner Hähnle, Werner Kernig	Verification of Switch-Level Designs with Many-Valued Logic.	LPAR	1993	DBLP DOI BibTeX RDF
7	Matthias Baaz, Christian G. Fermüller, Arie Ovrutcki, Richard Zach	MULTILOG: A System for Axiomatizing Many-valued Logics.	LPAR	1993	DBLP DOI BibTeX RDF
7	Churn-Jung Liau, Bertrand I-Peng Lin	Reasoning about Higher Order Uncertainty in Possiblistic Logic.	ISMIS	1993	DBLP DOI BibTeX RDF
7	Allen L. Brown Jr., Surya Mantha, Toshiro Wakayama	A Logical Reconstruction of Constraint Relaxation Hierarchies in Logic Programming.	ISMIS	1993	DBLP DOI BibTeX RDF
7	Geoffrey Smith 0001	Polymorphic Type Inference with Overloading and Subtyping.	TAPSOFT	1993	DBLP DOI BibTeX RDF
7	Robert Harper 0001, Mark Lillibridge	Explicit Polymorphism and CPS Conversion.	POPL	1993	DBLP DOI BibTeX RDF
7	Werner Stephan 0001, Andreas Wolpers	A Calculus for Higher Order Procedures with Global Variables.	MFCS	1993	DBLP DOI BibTeX RDF
7	Saumya K. Debray	Efficient Dataflow Analysis of Logic Programs.	J. ACM	1992	DBLP DOI BibTeX RDF	PROLOG, program analysis
7	Sonia Bergamaschi, Claudio Sartori 0001	On Taxonomic Reasoning in Conceptual Design.	ACM Trans. Database Syst.	1992	DBLP DOI BibTeX RDF	schema consistency, schema minimality, taxonomic reasoning, semantic models
7	Rolf Socher-Ambrosius	A Goal Oriented Strategy Based on Completion.	ALP	1992	DBLP DOI BibTeX RDF
7	Andrew K. Wright	Typing References by Effect Inference.	ESOP	1992	DBLP DOI BibTeX RDF
7	Martin Protzen	Disproving Conjectures.	CADE	1992	DBLP DOI BibTeX RDF
7	Bernhard Beckert, Reiner Hähnle	An Improved Method for Adding Equality to Free Variable Semantic Tableaux.	CADE	1992	DBLP DOI BibTeX RDF
7	Marcelo Finger, Dov M. Gabbay	Updating Atomic Information in Labelled Database Systems.	ICDT	1992	DBLP DOI BibTeX RDF
7	Lunjin Lu, Peter Greenfield	Abstract fixpoint semantics and abstract procedural semantics of definite logic programs.	ICCL	1992	DBLP DOI BibTeX RDF
7	Michele Boreale, Rocco De Nicola	Testing Equivalence for Mobile Processes (Extended Abstract).	CONCUR	1992	DBLP DOI BibTeX RDF
7	Juan Carlos González Moreno, Maria Teresa Hortalá-González, Mario Rodríguez-Artalejo	On the Completeness of Narrowing as the Operational Semantics of Functional Logic Programming.	CSL	1992	DBLP DOI BibTeX RDF
7	Luís Moniz Pereira, Luís Caires, José Júlio Alferes	SLWV - A Theorem Prover for Logic Programming.	ELP	1992	DBLP DOI BibTeX RDF
7	Harold Boley	A Direct Semantic Characterization of RELFUN.	ELP	1992	DBLP DOI BibTeX RDF
7	I. C. You, Chong-Nam Chu, Rangasami L. Kashyap	Symbolic representation of three-dimensional objects to aid local and global shape analysis for defect prediction of casting design.	Appl. Intell.	1991	DBLP DOI BibTeX RDF	Casting design, pattern model, feature, skeleton extraction
7	Martín Abadi, Luca Cardelli, Benjamin C. Pierce, Gordon D. Plotkin	Dynamic Typing in a Statically Typed Language.	ACM Trans. Program. Lang. Syst.	1991	DBLP DOI BibTeX RDF	theory
7	Martin C. Henson	Safe Positive Induction in the Programming Logic TK.	RCLP	1991	DBLP DOI BibTeX RDF
7	Giuseppe Attardi, Mauro Gaspari	Multilanguage Interoperability.	PLILP	1991	DBLP DOI BibTeX RDF
7	Sergio Antoy	Lazy Evaluation in Logic.	PLILP	1991	DBLP DOI BibTeX RDF
7	Nancy A. Lynch, Frits W. Vaandrager	Forward and Backward Simulations for Timing-Based Systems.	REX Workshop	1991	DBLP DOI BibTeX RDF	timing-based systems, backward simulations, forward-backward simulations, backward-forward simulations, history variables, prophecy variables, history relations, prophecy relations, Simulations, real-time, timed automata, refinement mappings, forward simulations
7	Steven Klusener	Abstraction in Real Time Process Algebra.	REX Workshop	1991	DBLP DOI BibTeX RDF	& Phrases Real Time, Abstraction, Process Algebra, Protocol Verification, ACP
7	Neal Nelson	Primitive Recursive Functionals with Dependent Types.	MFPS	1991	DBLP DOI BibTeX RDF
7	Philippe Balbiani	A Modal Semantics for the Negation as Failure and the Closed World Assumption Rules.	STACS	1991	DBLP DOI BibTeX RDF	logic programming with negation, modal logic, declarative semantics
7	Jan Friso Groote, Alban Ponse	Process Algebra with Guards - Combining Hoare Logic with Process Algebra (Extended Abstract).	CONCUR	1991	DBLP DOI BibTeX RDF
7	Steven Klusener	Completeness in Real Time Process Algebra.	CONCUR	1991	DBLP DOI BibTeX RDF	& Phrases Real Time, Integration, Process Algebra, SOS, ACP
7	Antonio Brogi, Evelina Lamma, Paola Mello	Open Logic Theories.	ELP	1991	DBLP DOI BibTeX RDF
7	Lars-Henrik Eriksson	A Finitary Version of the Calculus of Partial Inductive Defintions.	ELP	1991	DBLP DOI BibTeX RDF
7	Joseph Y. Halpern, John H. Williams, Edward L. Wimmers	Completeness of Rewrite Rules and Rewrite Strategies for FP	J. ACM	1990	DBLP DOI BibTeX RDF	FP
7	Martín Abadi, Zohar Manna	Nonclausal Deduction in First-Order Temporal Logic	J. ACM	1990	DBLP DOI BibTeX RDF