Search results for "Higher-order-logic"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
4	Anand Chavan, Shiu-Kai Chin, Shahid Ikram, Jang Dae Kim, Juin-Yeu Zu	Extending VLSI design with higher-order logic. (PDF / PS)	ICCD	1995	DBLP DOI BibTeX RDF	Cambridge Higher-Order Logic theorem-prover, microprogram sequencer, Am2910, VLSI, formal verification, formal verification, logic testing, theorem proving, logic design, logic CAD, VLSI design, higher-order logic, theorem-prover, design environment, instruction-set architecture, VLSI CAD
3	Florian Haftmann	From higher-order logic to Haskell: there and back again.	PEPM	2010	DBLP DOI BibTeX RDF	code generation, theorem proving, haskell, higher-order logic, isabelle
3	Franz Regensburger	HOLCF: Higher Order Logic of Computable Functions.	TPHOLs	1995	DBLP DOI BibTeX RDF
3	Joakim von Wright	Representing Higher-Order Logic Proofs in HOL.	TPHOLs	1994	DBLP DOI BibTeX RDF
3	Holger Busch	First-Order Automation for Higher-Order-Logic Theorem Proving.	TPHOLs	1994	DBLP DOI BibTeX RDF
3	Ching-Tsun Chou	A Formal Theory of Undirected Graphs in Higher-Order Logic.	TPHOLs	1994	DBLP DOI BibTeX RDF
3	Jeffrey J. Joyce, Nancy A. Day, Michael R. Donat	S: A Machine Readable Specification Notation based on Higher Order Logic.	TPHOLs	1994	DBLP DOI BibTeX RDF
3	Ching-Tsun Chou	Mechanical Verification of Distributed Algorithms in Higher-Order Logic.	TPHOLs	1994	DBLP DOI BibTeX RDF
3	Klaus Schneider, Ramayya Kumar, Thomas Kropf	Alternative Proof Procedures for Finite-State Machines in Higher-Order Logic.	HUG	1993	DBLP DOI BibTeX RDF
3	Victor Carreño	Verification in Higher Order Logic of Mutual Exclusion Algorithm.	HUG	1993	DBLP DOI BibTeX RDF
3	Matthew J. Morley	Safety in Railway Signalling Data: A Behavioural Analysis.	HUG	1993	DBLP DOI BibTeX RDF	application specific languages, Safety-critical systems, higher-order logic, railway signalling
3	Ralph-Johan Back, Joakim von Wright	Predicate Transformers and Higher Order Logic.	REX Workshop	1992	DBLP DOI BibTeX RDF	nondeterminism, higher order logic, state spaces, weakest preconditions, procedures, Stepwise refinement, predicate transformers, HOL, semantics of programming languages, total correctness
3	Albert John Camilleri	Mechanizing CSP Trace Theory in Higher Order Logic.	IEEE Trans. Software Eng.	1990	DBLP DOI BibTeX RDF	mechanising CSP trace theory, general-purpose theorem prover, formal specification, theorem proving, formal logic, higher order logic, communicating sequential processes
2	Geoff Sutcliffe, Christoph Benzmüller, Chad E. Brown, Frank Theiss	Progress in the Development of Automated Theorem Proving for Higher-Order Logic.	CADE	2009	DBLP DOI BibTeX RDF
2	Osman Hasan, Sofiène Tahar	Performance Analysis and Functional Verification of the Stop-and-Wait Protocol in HOL.	J. Autom. Reasoning	2009	DBLP DOI BibTeX RDF	Real-time systems, Communication protocols, Higher-order-logic, Probability theory, HOL theorem prover
2	Christoph Benzmüller, Florian Rabe, Geoff Sutcliffe	THF0 - The Core of the TPTP Language for Higher-Order Logic.	IJCAR	2008	DBLP DOI BibTeX RDF
2	Christoph Benzmüller, Lawrence C. Paulson, Frank Theiss, Arnaud Fietzke	LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description).	IJCAR	2008	DBLP DOI BibTeX RDF
2	Linna Li, Wei Zhang	Higher-Order Logic Recommender System.	Web Intelligence/IAT Workshops	2008	DBLP DOI BibTeX RDF
2	Linna Li, Bingru Yang, Fan Zhang	Clustering for Complex Structured Data Based on Higher-Order Logic.	CSSE	2008	DBLP DOI BibTeX RDF
2	Jia Meng, Lawrence C. Paulson	Translating Higher-Order Clauses to First-Order Clauses.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	Interactive theorem provers, Clause translation, First-order logic, Higher-order logic
2	James Lipton, Susana Nieva	Higher-Order Logic Programming Languages with Constraints: A Semantics.	TLCA	2007	DBLP DOI BibTeX RDF
2	Guodong Li, Konrad Slind	Compilation as Rewriting in Higher Order Logic.	CADE	2007	DBLP DOI BibTeX RDF
2	Norbert Völker	HOL2P - A System of Classical Higher Order Logic with Second Order Polymorphism.	TPHOLs	2007	DBLP DOI BibTeX RDF
2	Guodong Li, Scott Owens, Konrad Slind	Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic.	ESOP	2007	DBLP DOI BibTeX RDF
2	Guillaume Burel	Unbounded Proof-Length Speed-Up in Deduction Modulo.	CSL	2007	DBLP DOI BibTeX RDF	rewriting, arithmetic, higher order logic, proof theory
2	Osman Hasan, Sofiène Tahar	Verification of Probabilistic Properties in HOL Using the Cumulative Distribution Function.	IFM	2007	DBLP DOI BibTeX RDF	Higher-Order-Logic, Interactive Theorem Proving, HOL, Probabilistic Systems, Cumulative Distribution Function
2	Xiaobing Wu	An Inductive Learning System for XML Documents.	ILP	2007	DBLP DOI BibTeX RDF	precision-recall, knowledge representation, higher-order logic, XML documents, decision-tree learning
2	Oliver Pell	Verification of FPGA Layout Generators in Higher-Order Logic.	J. Autom. Reasoning	2006	DBLP DOI BibTeX RDF	layout description, circuit verification, FPGA, theorem proving
2	Alexander Krauss	Partial Recursive Functions in Higher-Order Logic.	IJCAR	2006	DBLP DOI BibTeX RDF
2	Allen Van Gelder, Geoff Sutcliffe	Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation.	IJCAR	2006	DBLP DOI BibTeX RDF
2	Kee Siong Ng	(Agnostic) PAC Learning Concepts in Higher-Order Logic.	ECML	2006	DBLP DOI BibTeX RDF
2	Herman Geuvers	(In)consistency of Extensions of Higher Order Logic and Type Theory.	TYPES	2006	DBLP DOI BibTeX RDF
2	Steven Obua	Checking Conservativity of Overloaded Definitions in Higher-Order Logic.	RTA	2006	DBLP DOI BibTeX RDF
2	Michael J. C. Gordon, Warren A. Hunt Jr., Matt Kaufmann, James Reynolds	An embedding of the ACL2 logic in HOL.	ACL2	2006	DBLP DOI BibTeX RDF	HOL4, proof oracle, sound translation, verification, formal methods, logic, first-order logic, higher-order logic, ACL2, HOL
2	Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough	Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations.	POPL	2006	DBLP DOI BibTeX RDF	specification, TCP/IP, network protocols, operational semantics, API, conformance testing, higher-order logic, sockets, HOL
2	Brigitte Pientka	Verifying Termination and Reduction Properties about Higher-Order Logic Programs.	J. Autom. Reasoning	2005	DBLP DOI BibTeX RDF	termination, Logical frameworks
2	Serge Autexier	On the Dynamic Increase of Multiplicities in Matrix Proof Methods for Classical Higher-Order Logic.	TABLEAUX	2005	DBLP DOI BibTeX RDF
2	Daniel Cabeza, Manuel V. Hermenegildo, James Lipton	Hiord: A Type-Free Higher-Order Logic Programming Language with Predicate Abstraction.	ASIAN	2004	DBLP DOI BibTeX RDF
2	Thomas Gärtner, John W. Lloyd, Peter A. Flach	Kernels and Distances for Structured Data.	Machine Learning	2004	DBLP DOI BibTeX RDF	kernel methods, inductive logic programming, higher-order logic, instance-based learning, structured data
2	Farhad Mehta, Tobias Nipkow	Proving Pointer Programs in Higher-Order Logic.	CADE	2003	DBLP DOI BibTeX RDF
2	Viktor K. Sabelfeld, Kai Kapp	Numeric Types in Formal Synthesis.	Ershov Memorial Conference	2003	DBLP DOI BibTeX RDF	correct hardware synthesis, formal specification, higher-order logic, theorem prover, arithmetic operations
2	Michael J. C. Gordon	Validating the PSL/Sugar Semantics Using Automated Reasoning.	Formal Asp. Comput.	2003	DBLP DOI BibTeX RDF	Accellera, Property language, Sugar, Model checking, Semantics, Formal verification, Theorem proving, Higher-order logic, PSL, HOL
2	Peter B. Andrews	Herbrand Award Acceptance Speech.	J. Autom. Reasoning	2003	DBLP DOI BibTeX RDF	Herbrand's theorem, TPS, higher-order logic
2	Chuck Liang	Compiler Construction in Higher Order Logic Programming.	PADL	2002	DBLP DOI BibTeX RDF
2	Brigitte Pientka	A Proof-Theoretic Foundation for Tabled Higher-Order Logic Programming.	ICLP	2002	DBLP DOI BibTeX RDF
2	Graeme Smith, Florian Kammüller, Thomas Santen	Encoding Object-Z in Isabelle/HOL.	ZB	2002	DBLP DOI BibTeX RDF	reference semantics, Object-Z, higher-order logic, Isabelle
2	Brigitte Pientka	Termination and Reduction Checking for Higher-Order Logic Programs.	IJCAR	2001	DBLP DOI BibTeX RDF
2	Natarajan Shankar	Using Decision Procedures with a Higher-Order Logic.	TPHOLs	2001	DBLP DOI BibTeX RDF
2	Matt Fairtlough, Michael Mendler, Xiaochun Cheng	Abstraction and Refinement in Higher Order Logic.	TPHOLs	2001	DBLP DOI BibTeX RDF
2	Marc Bezem	An Improved Extensionality Criterion for Higher-Order Logic Programs.	CSL	2001	DBLP DOI BibTeX RDF
2	Neophytos G. Michael, Andrew W. Appel	Machine Instruction Syntax and Semantics in Higher Order Logic.	CADE	2000	DBLP DOI BibTeX RDF
2	Marieke Huisman, Bart Jacobs	Inheritance in Higher Order Logic: Modeling and Reasoning.	TPHOLs	2000	DBLP DOI BibTeX RDF
2	Martin Hofmann, Francis Tang	Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover.	TPHOLs	2000	DBLP DOI BibTeX RDF
2	Stefan Berghofer, Tobias Nipkow	Proof Terms for Simply Typed Higher Order Logic.	TPHOLs	2000	DBLP DOI BibTeX RDF
2	Kurt Lichtner, Paulo S. C. Alencar, Donald D. Cowan	A Framework for Software Architecture Verification.	Australian Software Engineering Conference	2000	DBLP DOI BibTeX RDF	formal modeling, architecture description languages (ADLs), higher-order logic, Software architecture analysis
2	Zhan Naijun	Completeness of Higher-Order Duration Calculus.	CSL	2000	DBLP DOI BibTeX RDF	duration calculus higher-order logic interval temporal logic completeness
2	Gilles Dowek, Thérèse Hardin, Claude Kirchner	HOL-lambdasigma: An Intentional First-Order Expression of Higher-Order Logic.	RTA	1999	DBLP DOI BibTeX RDF
2	Wolfgang Naraschewski, Markus Wenzel	Object-Oriented Verification Based on Record Subtyping in Higher-Order Logic.	TPHOLs	1998	DBLP DOI BibTeX RDF
2	Marco Benini, Sara Kalvala, Dirk Nowotka	Program Abstraction in a Higher-Order Logic Framework.	TPHOLs	1998	DBLP DOI BibTeX RDF
2	James H. Andrews	Executing Formal Specifications by Translation to Higher Order Logic Programming.	TPHOLs	1997	DBLP DOI BibTeX RDF
2	Gilles Dowek	Proof Normalization for a First-Order Formulation of Higher-Order Logic.	TPHOLs	1997	DBLP DOI BibTeX RDF
2	Konrad Slind	Derivation and Use of Induction Schemes in Higher-Order Logic.	TPHOLs	1997	DBLP DOI BibTeX RDF
2	Randall W. Lichota, Grace L. Hammonds, Stephen H. Brackin	Verifying The Correctness Of Cryptographic Protocols Using "Convince".	ACSAC	1996	DBLP DOI BibTeX RDF	Convince, theorem proving component, commercial computer aided software engineering tool, StP/OMT, textual notations, Higher Order Logic theorem prover, protocols, cryptographic protocols, authentication protocols, front-end, belief logic, correctness verification, automated support
2	Stephen H. Brackin	A HOL extension of GNY for automatically analyzing cryptographic protocols.	CSFW	1996	DBLP DOI BibTeX RDF	HOL extension, automatically analyzing cryptographic protocols, higher order logic theory, authentication properties, protocol properties, hash operations, key-exchange algorithms, formal specification, cryptography, message authentication, access protocols, message authentication codes, multiple encryption, belief maintenance, belief logic
2	Martin Hofmann, Donald Sannella	On Behavioral Abstraction and Behavioural Satisfaction in Higher-Order Logic.	TAPSOFT	1995	DBLP DOI BibTeX RDF
2	Holger Busch	A Practical Method for Reasoning about Distributed Systems in a Theorem Prover.	TPHOLs	1995	DBLP DOI BibTeX RDF
2	Sten Agerholm, Michael J. C. Gordon	Experiments with ZF Set Theory in HOL and Isabelle.	TPHOLs	1995	DBLP DOI BibTeX RDF
2	Sten Agerholm	Non-primitive Recursive Function Definitions.	TPHOLs	1995	DBLP DOI BibTeX RDF
2	Paul Loewenstein	Formal Verification of Counterflow Pipeline Architecture.	TPHOLs	1995	DBLP DOI BibTeX RDF
2	B. M. Subraya, Anshul Kumar, Shashi Kumar	An HOL based framework for design of correct high level synthesizers.	VLSI Design	1995	DBLP DOI BibTeX RDF	HOL based framework, high level synthesizer design, design correctness guarantee, verifiable templates, synthesis module correctness, formal verification, high level synthesis, modularity, formal logic, higher order logic, verification process, formal framework
2	Juin-Yeu Lu, Shiu-Kai Chin	Generating Designs Using an Algorithmic Register Transfer Language with Formal Semantics.	TPHOLs	1994	DBLP DOI BibTeX RDF
2	Kim Dam Petersen	Graph model of LAMBDA in Higher Order Logic.	HUG	1993	DBLP DOI BibTeX RDF
2	Nancy A. Day, Jeffrey J. Joyce	The Semantics of Statecharts in HOL.	HUG	1993	DBLP DOI BibTeX RDF
2	Konrad Slind	AC Unification in HOL90.	HUG	1993	DBLP DOI BibTeX RDF
2	Juin-Yeu Lu, Shiu-Kai Chin	Linking HOL to a VLSI CAD System.	HUG	1993	DBLP DOI BibTeX RDF
2	Wai Wong	Modelling Bit Vectors in HOL: the word library.	HUG	1993	DBLP DOI BibTeX RDF
2	Dirk Eisenbiegler, Klaus Schneider, Ramayya Kumar	A Functional Approach for Formalizing Regular Hardware Structures.	HUG	1993	DBLP DOI BibTeX RDF
2	Klaus Schneider, Ramayya Kumar, Thomas Kropf	Eliminating Higher-Order Quantifiers to Obtain Decision Procedures for Hardware Verification.	HUG	1993	DBLP DOI BibTeX RDF
2	Mark Aagaard, Miriam Leeser, Phillip J. Windley	Toward a Super Duper Hardware Tactic.	HUG	1993	DBLP DOI BibTeX RDF
2	Alain Hui-Bon-Hoa	A Bottom-Up Interpreter for a Higher-Order Logic Programming Language.	PLILP	1992	DBLP DOI BibTeX RDF
2	Sreeranga P. Rajan	Executing HOL Specifications: Towards an Evaluation Semantics for Classical Higher Order Logic.	TPHOLs	1992	DBLP BibTeX RDF
2	Weidong Chen, David Scott Warren	Compilation of Predicate Abstractions in Higher-Order Logic Programming.	PLILP	1991	DBLP DOI BibTeX RDF
2	Paul Loewenstein, David L. Dill	Verification of a Multiprocessor Cache Protocol Using Simulation Relations and Higher-Order Logic.	CAV	1990	DBLP DOI BibTeX RDF
2	Jeffrey J. Joyce	Totally Verified Systems: Linking Verified Software to Verified Hardware.	Hardware Specification, Verification and Synthesis	1989	DBLP DOI BibTeX RDF	machine-assisted theorem proving, safety-critical systems, higher-order logic, hardware verification, compiler correctness
2	Amy P. Felty, Dale Miller	Specifying Theorem Provers in a Higher-Order Logic Programming Language.	CADE	1988	DBLP DOI BibTeX RDF
2	Shiu-Kai Chin, Edward P. Stabler, Kevin J. Greene	Using higher order logic and functional languages to synthesize correct hardware.	ICCL	1988	DBLP DOI BibTeX RDF
2	Peter B. Andrews	Connections and Higher-Order Logic.	CADE	1986	DBLP DOI BibTeX RDF
2	M. A. Nait Abdallah	AL-Khowarizmi: A Formal System for Higher-Order Logic Programming.	MFCS	1986	DBLP DOI BibTeX RDF
2	Dale Miller	Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs.	CADE	1984	DBLP DOI BibTeX RDF	Expansion Trees, ET-proofs, Matings, Higher-order Logic, Natural Deduction
2	George W. Ernst, Raymond J. Hookway	The Use of Higher Order Logic in Program Verification.	IEEE Trans. Computers	1976	DBLP DOI BibTeX RDF	inductive assertions, program verification, Heuristic search, higher order logic, mechanical theorem proving
1	Stefan Hetzl, Alexander Leitsch, Daniel Weller	CERES in higher-order logic.	Ann. Pure Appl. Logic	2011	DBLP DOI BibTeX RDF
1	Osman Hasan, Sofiène Tahar	Reasoning about conditional probabilities in a higher-order-logic theorem prover.	J. Applied Logic	2011	DBLP DOI BibTeX RDF
1	Christoph Benzmueller, Dov M. Gabbay, Valerio Genovese, Daniele Rispoli	Embedding and Automating Conditional Logics in Classical Higher-Order Logic	CoRR	2011	DBLP BibTeX RDF
1	Angelos Charalambidis, Konstantinos Handjopoulos, Panos Rondogiannis, William W. Wadge	Extensional Higher-Order Logic Programming	CoRR	2011	DBLP BibTeX RDF
1	Julian Backes, Chad E. Brown	Analytic Tableaux for Higher-Order Logic with Choice.	J. Autom. Reasoning	2011	DBLP DOI BibTeX RDF
1	Wihem Arsac, Luca Compagna, Samuel Paul Kaluvuri, Serena Elisa Ponta	Security validation tool for business processes.	SACMAT	2011	DBLP DOI BibTeX RDF
1	Alexander Krauss	Partial and Nested Recursive Function Definitions in Higher-order Logic.	J. Autom. Reasoning	2010	DBLP DOI BibTeX RDF
1	John Lloyd	Higher-Order Logic.	Encyclopedia of Machine Learning	2010	DBLP DOI BibTeX RDF
1	Julian Backes, Chad E. Brown	Analytic Tableaux for Higher-Order Logic with Choice.	IJCAR	2010	DBLP DOI BibTeX RDF
1	Niels Pahlavi	Higher-order Logic Learning and lambda-Progol.	ICLP (Technical Communications)	2010	DBLP DOI BibTeX RDF