Search results for "Higher-order-logic"

Hits ?▲	Authors	Title	Venue	Year	Link
15	Thomas Långbacka	A HOL Formalisation of the Temporal Logic of Actions.	TPHOLs	1994	DBLP DOI BibTeX RDF
15	Weidong Chen 0005, Michael Kifer, David Scott Warren	HILOG: A Foundation for Higher-Order Logic Programming.	J. Log. Program.	1993	DBLP DOI BibTeX RDF
15	Amy P. Felty	Implementing Tactics and Tacticals in a Higher-Order Logic Programming Language.	J. Autom. Reason.	1993	DBLP DOI BibTeX RDF
15	Thomas F. Melham	Higher Order Logic and Hardware Verification.		1993	DOI RDF
15	Luc J. M. Claesen, Michael J. C. Gordon (eds.)	Higher Order Logic Theorem Proving and its Applications, Proceedings of the IFIP TC10/WG10.2 Workshop HOL'92, Leuven, Belgium, 21-24 September 1992	TPHOLs	1993	DBLP BibTeX RDF
15	Bart Jacobs 0001, Thomas F. Melham	Translating Dependent Type Theory into Higher Order Logic.	TLCA	1993	DBLP DOI BibTeX RDF
15	Amy P. Felty	Encoding the Calculus of Constructions in a Higher-Order Logic	LICS	1993	DBLP DOI BibTeX RDF
15	Jeffrey J. Joyce, Carl-Johan H. Seger	The HOL-Voss System: Model-Checking inside a General-Purpose Theorem-Prover.	HUG	1993	DBLP DOI BibTeX RDF
15	Ching-Tsun Chou	Predicates, Temporal Logic, and Simulations.	HUG	1993	DBLP DOI BibTeX RDF
15	Andrew D. Gordon 0001	A Mechanisation of Name-Carrying Syntax up to Alpha-Conversion.	HUG	1993	DBLP DOI BibTeX RDF
15	Sreeranga P. Rajan, Jeffrey J. Joyce, Carl-Johan H. Seger	From Abstract Data Types to Shift Registers: A Case Study in Formal Specification and Verification at Differing Levels of Abstraction using Theorem Proving and Symbolic Simulation.	HUG	1993	DBLP DOI BibTeX RDF
15	David Lorge Parnas	Some Theorems We Should Prove.	HUG	1993	DBLP DOI BibTeX RDF
15	Elsa L. Gunter	A Broader Class of Trees for Recursive Type Definitions for HOL.	HUG	1993	DBLP DOI BibTeX RDF
15	Myra Van Inwegen, Elsa L. Gunter	HOL-ML.	HUG	1993	DBLP DOI BibTeX RDF
15	Monica Nesi	Value-Passing CCS in HOL.	HUG	1993	DBLP DOI BibTeX RDF
15	Laurent Théry	A Proof Development System for HOL.	HUG	1993	DBLP DOI BibTeX RDF
15	Zheng Zhu, Jeffrey J. Joyce, Carl-Johan H. Seger	Verification of the Tamarack-3 Microprocessor in a Hybrid Verification Environment.	HUG	1993	DBLP DOI BibTeX RDF
15	Kees G. W. Goossens	Stucture and Behaviour in Hardware Verification.	HUG	1993	DBLP DOI BibTeX RDF
15	Sara Kalvala	Using Isabelle to Prove Simple Theorems.	HUG	1993	DBLP DOI BibTeX RDF
15	Rachel E. O. Roxas	A HOL Package for Reasoning about Relations Defined by Mutual Induction.	HUG	1993	DBLP DOI BibTeX RDF
15	Don Syme	Reasoning with the Formal Definition of Standard ML in HOL.	HUG	1993	DBLP DOI BibTeX RDF
15	Stephen H. Brackin, Shiu-Kai Chin	Server-Process Restrictiveness in HOL.	HUG	1993	DBLP DOI BibTeX RDF
15	I. S. W. B. Prasetya	Formalization of Variables Access Constraints to Support Compositionality of Liveness Properties.	HUG	1993	DBLP DOI BibTeX RDF
15	Flemming Andersen, Kim Dam Petersen, Jimmi S. Pettersson	Program Verification using HOL-UNITY.	HUG	1993	DBLP DOI BibTeX RDF
15	John M. Rushby, Mandayam K. Srivas	Using PVS to Prove Some Theorems Of David Parnas.	HUG	1993	DBLP DOI BibTeX RDF
15	I. S. W. B. Prasetya	On the Style of Mechanical Proving.	HUG	1993	DBLP DOI BibTeX RDF
15	Tej Arora, Tony Leung, Karl N. Levitt, E. Thomas Schubert, Phillip J. Windley	Report on the UCD Microcoded Viper Verification Project.	HUG	1993	DBLP DOI BibTeX RDF
15	John Harrison 0001	A HOL Decision Procedure for Elementary Real Algebra.	HUG	1993	DBLP DOI BibTeX RDF
15	Cui Zhang, Robert J. Shaw, Ronald A. Olsson, Karl N. Levitt, Myla Archer, Mark R. Heckman, Gregory D. Benson	Mechanizing a Programming Logic for the Concurrent Programming Language microSR in HOL.	HUG	1993	DBLP DOI BibTeX RDF
15	Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi	TPS: An Interactive and Automatic Tool for Proving Theorems of Type Theory.	HUG	1993	DBLP DOI BibTeX RDF
15	Anthony McIsaac	A Formalization of Abstraction in LAMBDA.	HUG	1993	DBLP DOI BibTeX RDF
15	David A. Fura, Phillip J. Windley, Arun K. Somani	Abstraction Techniques for Modeling Real-World Interface Chips.	HUG	1993	DBLP DOI BibTeX RDF
15	Catia M. Angelo, Luc J. M. Claesen, Hugo De Man	Degrees of Formality in Shallow Embedding Hardware Description Languages in HOL.	HUG	1993	DBLP DOI BibTeX RDF
15	Sten Agerholm	Domain Theory in HOL.	HUG	1993	DBLP DOI BibTeX RDF
15	Sofiène Tahar, Ramayya Kumar	Implementing a Methodology for Formally Verifying RISC Processors in HOL.	HUG	1993	DBLP DOI BibTeX RDF
15	John Harrison 0001, Laurent Théry	Extending the HOL Theorem Prover with a Computer Algebra System to Reason about the Reals.	HUG	1993	DBLP DOI BibTeX RDF
15	Paul Loewenstein	Verification of a Multiprocessor Cache Protocol Using Simulation Relations and Higher-Order Logic.	Formal Methods Syst. Des.	1992	DBLP DOI BibTeX RDF
15	Gopalan Nadathur, Frank Pfenning	The Type System of a Higher-Order Logic Programming Language.	Types in Logic Programming	1992	DBLP BibTeX RDF
15	Wenchang Fang, Jung-Hong Kao	Set-Of-Support Strategy for Higher-Order Logic.	CTRS	1992	DBLP DOI BibTeX RDF
15	Ralph-Johan Back	Refinement Calculus, Lattices and Higher Order Logic.	NATO ASI PDC	1992	DBLP DOI BibTeX RDF
15	Andrew D. Gordon 0001	The Formal Definition of a Synchronous Hardware-Description Language in Higher Order Logic.	ICCD	1992	DBLP DOI BibTeX RDF
15	Rachel Cardell-Oliver	A Mechanized Theory for the Verification of Real-Time Program Code using Higher Order Logic.	FTRTFT	1992	DBLP DOI BibTeX RDF
15	Cao Feng, Stephen H. Muggleton	Towards Inductive Generalization in Higher Order Logic.	ML	1992	DBLP DOI BibTeX RDF
15	Wai Wong	A formal theory of railway track networks in higher-order logic and its applications in interlocking design.		1992	RDF
15	Elsa L. Gunter	Why we can't have SML-style datatype Declarations in HOL.	TPHOLs	1992	DBLP BibTeX RDF
15	Saraswati Kalvala, Myla Archer, Karl N. Levitt	Implementation and Use of Annotations in HOL.	TPHOLs	1992	DBLP BibTeX RDF
15	Joakim von Wright, Jukka Hekanaho, P. Luostarinen, Thomas Långbacka	Mechanising some Advanced Refinement Concepts.	TPHOLs	1992	DBLP BibTeX RDF
15	Paul Loewenstein	A Formal Theory of Simulations Between Infinite Automata.	TPHOLs	1992	DBLP BibTeX RDF
15	Jing Pan, Karl N. Levitt, Myla Archer, Saraswati Kalvala	Towards a Formal Verification of a Floating Point Coprocessor and its Composition with a Central Processing Unit.	TPHOLs	1992	DBLP BibTeX RDF
15	Phillip J. Windley	Abstract Theories in HOL.	TPHOLs	1992	DBLP BibTeX RDF
15	Konrad Slind	Adding New Rules to an LCF-style Logic Implementation.	TPHOLs	1992	DBLP BibTeX RDF
15	Richard J. Boulton	Boyer-Moore Automation for the HOL System.	TPHOLs	1992	DBLP BibTeX RDF
15	Holger Busch	Unification Based Induction.	TPHOLs	1992	DBLP BibTeX RDF
15	Garrel Pottinger	A Classical Type Theory with Transfinite Types.	TPHOLs	1992	DBLP BibTeX RDF
15	Kees G. W. Goossens	Operational Semantics Based on Formal Symbolic Simulation.	TPHOLs	1992	DBLP BibTeX RDF
15	Richard J. Boulton	A Lazy Approach to Fully-Expansive Theorem Proving.	TPHOLs	1992	DBLP BibTeX RDF
15	John Harrison 0001	Constructing the real numbers in HOL.	TPHOLs	1992	DBLP BibTeX RDF
15	Li-Guo Wang	Deriving a Correct Computer.	TPHOLs	1992	DBLP BibTeX RDF
15	Massimo Bombana, Patrizia Cavalloro, Giuseppe Zaza	Specification and Formal Synthesis of Digital Circuits.	TPHOLs	1992	DBLP BibTeX RDF
15	William L. Harrison, Myla Archer, Karl N. Levitt	A HOL Mechanisation of the Axiomatic Semantics of a Simple Distributed Programming Language.	TPHOLs	1992	DBLP BibTeX RDF
15	Nancy A. Day	A Comparison between Statecharts and State Transition Assertions.	TPHOLs	1992	DBLP BibTeX RDF
15	Myla Archer, George Fink, Lie Yang	Linking Other Theorem Provers to HOL Using PM: Proof Manager.	TPHOLs	1992	DBLP BibTeX RDF
15	Ching-Tsun Chou	A Note on Interactive Theorem Proving with Theorem Continuation Functions.	TPHOLs	1992	DBLP BibTeX RDF
15	Rachel Cardell-Oliver, Roger Hale, John Herbert	An Embedding of Timed Transition Systems in HOL.	TPHOLs	1992	DBLP BibTeX RDF
15	Mark van der Voort	Introducing well-founded function definitions in HOL.	TPHOLs	1992	DBLP BibTeX RDF
15	Klaus Schneider 0001, Ramayya Kumar, Thomas Kropf	Efficient Representation and Computation of Tableau Proofs.	TPHOLs	1992	DBLP BibTeX RDF
15	Mark D. Aagaard, Miriam Leeser	A Methodology for Reusable Hardware Proofs.	TPHOLs	1992	DBLP BibTeX RDF
15	Roger B. Hughes, M. D. Francis, Simon Finn, Gerry Musgrave	Formal Tools in Tri-State Design in Busses.	TPHOLs	1992	DBLP BibTeX RDF
15	Monica Nesi	Formalizing a Modal Logic for CSS in the HOL Theorem Prover.	TPHOLs	1992	DBLP BibTeX RDF
15	Kelly M. Hall, Phillip J. Windley	Simulating Microprocessors from Formal Specifications.	TPHOLs	1992	DBLP BibTeX RDF
15	Michael McAllister	Machine Abstraction in Microprocessor Specification.	TPHOLs	1992	DBLP BibTeX RDF
15	Jim Alves-Foss	Modelling Non-Deterministic System in HOL.	TPHOLs	1992	DBLP BibTeX RDF
15	Roger B. Hughes, Gerry Musgrave	Design-Flow Graph Partitioning.	TPHOLs	1992	DBLP BibTeX RDF
15	Paul Curzon	Deriving Correctness Properties of Compiled Code.	TPHOLs	1992	DBLP BibTeX RDF
15	Klaus Schneider 0001, Ramayya Kumar, Thomas Kropf	Modelling Generic Hardware Structures by Abstract Datatypes.	TPHOLs	1992	DBLP BibTeX RDF
15	Ching-Tsun Chou	A Sequent Formulation of a Logic of Predicates in HOL.	TPHOLs	1992	DBLP BibTeX RDF
15	Catia M. Angelo, Luc J. M. Claesen, Hugo De Man	The Formal Semantics Definition of a Multi-Rate DSP Specification Language in HOL.	TPHOLs	1992	DBLP BibTeX RDF
15	John Van Tassel	A Formalisation of the VHDL Simulation Cycle.	TPHOLs	1992	DBLP BibTeX RDF
15	Thomas F. Melham	The HOL Logic Extended with Quantification over Type Variables.	TPHOLs	1992	DBLP BibTeX RDF
15	Monica Nesi	Mechanizing a Proof by Induction of Process Algebrs Specifications in Higher Order Logic.	CAV	1991	DBLP DOI BibTeX RDF
15	Shiu-Kai Chin, Graham M. Birtwistle	Implementing and Verifying Finite-State Machines Using Types in Higher-Order Logic.	TPHOLs	1991	DBLP BibTeX RDF
15	Jim Alves-Foss, Karl N. Levitt	Mechanical Verification of Secure Distributed Systems in Higher Order Logic.	TPHOLs	1991	DBLP BibTeX RDF
15	X. Wang, Edward P. Stabler	Formalization of VHDL Synthesis Procedure in Higher-Order Logic.	TPHOLs	1991	DBLP BibTeX RDF
15	Shiu-Kai Chin	Verifying Arithmetic Hardware in Higher-Order Logic.	TPHOLs	1991	DBLP BibTeX RDF
15	Rachel Cardell-Oliver	Using Higher Order Logic for Modelling Real-Time Protocols.	TAPSOFT, Vol.2	1991	DBLP DOI BibTeX RDF
15	Jim Alves-Foss, Karl N. Levitt	Verification of Secure Distributed Systems in Higher Order Logic: A Modular Approach Using Generic Components.	S&P	1991	DBLP DOI BibTeX RDF
15	Ralph-Johan Back, Joakim von Wright	Refinement Concepts Formalised in Higher Order Logic.	Formal Aspects Comput.	1990	DBLP DOI BibTeX RDF
15	Christoph Kreitz	The Representation of Program Synthesis in Higher Order Logic.	GWAI	1990	DBLP DOI BibTeX RDF
15	Dale Miller 0001	Higher-Order Logic Programming.	ICLP	1990	DBLP BibTeX RDF
15	Paul Loewenstein, David L. Dill	Verification of Multiprocessor Cache Protocol Using Simulation Relations and Higher-Order Logic.	CAV (DIMACS/AMS volume)	1990	DBLP DOI BibTeX RDF
15	Ralph-Johan Back, Joakim von Wright	Refinement Concepts Formalized in Higher Order Logic.	Programming Concepts and Methods	1990	DBLP BibTeX RDF
15	Peter B. Andrews	On Connections and Higher-Order Logic.	J. Autom. Reason.	1989	DBLP DOI BibTeX RDF
15	Paul Loewenstein	Reasoning about State Machines in Higher-Order Logic.	Hardware Specification, Verification and Synthesis	1989	DBLP DOI BibTeX RDF
15	Paul Loewenstein	Formal verification of state-machines using higher-order logic.	ICCD	1989	DBLP DOI BibTeX RDF
15	Sanjay Manchanda	"Higher-Order" Logic As a Data Model.	DBPL	1989	DBLP BibTeX RDF
15	Per Kreuger	A Higher Order Logic Parser for Natural Language Implemented in Lambda Prolog.	AIMSA	1988	DBLP BibTeX RDF
15	Glenn H. MacEwen, David B. Skillicorn	Using Higher-order Logic for Modular Specification of Real-time Distributed Systems.	FTRTFT	1988	DBLP DOI BibTeX RDF
15	Jeffrey J. Joyce	Formal Specification and Verification of Asynchronous Processes in Higher-Order Logic.	Specification and Verification of Concurrent Systems	1988	DBLP BibTeX RDF
15	Daniel Leivant	Characterization of complexity classes in higher-order logic.	SCT	1987	DBLP BibTeX RDF
15	Thierry Coquand, Thomas Ehrhard	An Equational Presentation of Higher Order Logic.	Category Theory and Computer Science	1987	DBLP DOI BibTeX RDF