Search results for "Higher-order-logic"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
80	Anand Chavan, Shiu-Kai Chin, Shahid Ikram, Jang Dae Kim, Juin-Yeu Zu	Extending VLSI design with higher-order logic.	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
50	Holger Busch	First-Order Automation for Higher-Order-Logic Theorem Proving.	TPHOLs	1994	DBLP DOI BibTeX RDF
49	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
49	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
49	Franz Regensburger	HOLCF: Higher Order Logic of Computable Functions.	TPHOLs	1995	DBLP DOI BibTeX RDF
48	Gilles Dowek	Proof Normalization for a First-Order Formulation of Higher-Order Logic.	TPHOLs	1997	DBLP DOI BibTeX RDF
46	Dale Miller 0001	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
44	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
44	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
44	Zhenyu Qian	Higher-Order Equational Logic Programming.	POPL	1994	DBLP DOI BibTeX RDF
42	Naijun Zhan	Completeness of Higher-Order Duration Calculus.	CSL	2000	DBLP DOI BibTeX RDF	duration calculus higher-order logic interval temporal logic completeness
40	Ching-Tsun Chou	A Formal Theory of Undirected Graphs in Higher-Order Logic.	TPHOLs	1994	DBLP DOI BibTeX RDF
39	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
39	Klaus Schneider 0001, Ramayya Kumar, Thomas Kropf	Alternative Proof Procedures for Finite-State Machines in Higher-Order Logic.	HUG	1993	DBLP DOI BibTeX RDF
39	Guillaume Burel	Unbounded Proof-Length Speed-Up in Deduction Modulo.	CSL	2007	DBLP DOI BibTeX RDF	rewriting, arithmetic, higher order logic, proof theory
37	Amy P. Felty, Dale Miller 0001	Specifying Theorem Provers in a Higher-Order Logic Programming Language.	CADE	1988	DBLP DOI BibTeX RDF
37	Martin Hofmann 0001, Francis Tang	Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover.	TPHOLs	2000	DBLP DOI BibTeX RDF
36	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
35	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
35	Joakim von Wright	Representing Higher-Order Logic Proofs in HOL.	TPHOLs	1994	DBLP DOI BibTeX RDF
35	Ching-Tsun Chou	Mechanical Verification of Distributed Algorithms in Higher-Order Logic.	TPHOLs	1994	DBLP DOI BibTeX RDF
35	Victor Carreño	Verification in Higher Order Logic of Mutual Exclusion Algorithm.	HUG	1993	DBLP DOI BibTeX RDF
35	Jia Meng, Lawrence C. Paulson	Translating Higher-Order Clauses to First-Order Clauses.	J. Autom. Reason.	2008	DBLP DOI BibTeX RDF	Interactive theorem provers, Clause translation, First-order logic, Higher-order logic
34	Graeme Smith 0001, 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
34	Flavio Antonio Ferrarotti, Jose Maria Turull Torres	Arity and Alternation: A Proper Hierarchy in Higher Order Logics.	FoIKS	2006	DBLP DOI BibTeX RDF
34	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
33	Brigitte Pientka	A Proof-Theoretic Foundation for Tabled Higher-Order Logic Programming.	ICLP	2002	DBLP DOI BibTeX RDF
33	Michael J. C. Gordon	Validating the PSL/Sugar Semantics Using Automated Reasoning.	Formal Aspects Comput.	2003	DBLP DOI BibTeX RDF	Accellera, Property language, Sugar, Model checking, Semantics, Formal verification, Theorem proving, Higher-order logic, PSL, HOL
33	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
33	Kee Siong Ng	(Agnostic) PAC Learning Concepts in Higher-Order Logic.	ECML	2006	DBLP DOI BibTeX RDF
32	Linna Li, Bingru Yang, Fan Zhang	Clustering for Complex Structured Data Based on Higher-Order Logic.	CSSE (4)	2008	DBLP DOI BibTeX RDF
32	Natarajan Shankar	Using Decision Procedures with a Higher-Order Logic.	TPHOLs	2001	DBLP DOI BibTeX RDF
32	Flavio Antonio Ferrarotti, Jose Maria Turull Torres	Arity and alternation: a proper hierarchy in higher order logics.	Ann. Math. Artif. Intell.	2007	DBLP DOI BibTeX RDF	Mathematics Subject Classifications (2000) 03C13, 68Q19, 03C85
32	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
31	Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith 0008, 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
31	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
31	Chuck C. Liang	Compiler Construction in Higher Order Logic Programming.	PADL	2002	DBLP DOI BibTeX RDF
31	Max Wisniewski, Alexander Steen	Embedding of Quantified Higher-Order Nominal Modal Logic into Classical Higher-Order Logic.	ARQNL@IJCAR	2014	DBLP DOI BibTeX RDF
31	Kim Dam Petersen	Graph model of LAMBDA in Higher Order Logic.	HUG	1993	DBLP DOI BibTeX RDF
31	Sreeranga P. Rajan	Executing HOL Specifications: Towards an Evaluation Semantics for Classical Higher Order Logic.	TPHOLs	1992	DBLP BibTeX RDF
30	Linna Li, Wei Zhang	Higher-Order Logic Recommender System.	Web Intelligence/IAT Workshops	2008	DBLP DOI BibTeX RDF
30	Klaus Schneider 0001, Ramayya Kumar, Thomas Kropf	Eliminating Higher-Order Quantifiers to Obtain Decision Procedures for Hardware Verification.	HUG	1993	DBLP DOI BibTeX RDF
30	Osman Hasan, Sofiène Tahar	Performance Analysis and Functional Verification of the Stop-and-Wait Protocol in HOL.	J. Autom. Reason.	2009	DBLP DOI BibTeX RDF	Real-time systems, Communication protocols, Higher-order-logic, Probability theory, HOL theorem prover
29	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
29	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
29	Thomas Gärtner 0001, John W. Lloyd, Peter A. Flach	Kernels and Distances for Structured Data.	Mach. Learn.	2004	DBLP DOI BibTeX RDF	kernel methods, inductive logic programming, higher-order logic, instance-based learning, structured data
29	Peter B. Andrews	Herbrand Award Acceptance Speech.	J. Autom. Reason.	2003	DBLP DOI BibTeX RDF	Herbrand's theorem, TPS, higher-order logic
29	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
29	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
29	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
29	Marc Bezem	An Improved Extensionality Criterion for Higher-Order Logic Programs.	CSL	2001	DBLP DOI BibTeX RDF
29	M. A. Nait Abdallah	AL-Khowarizmi: A Formal System for Higher-Order Logic Programming.	MFCS	1986	DBLP DOI BibTeX RDF
28	Gopalan Nadathur, Dale Miller 0001	Higher-Order Horn Clauses	J. ACM	1990	DBLP DOI BibTeX RDF
28	Wihem Arsac, Luca Compagna, Samuel Paul Kaluvuri, Serena Elisa Ponta	Security validation tool for business processes.	SACMAT	2011	DBLP DOI BibTeX RDF
27	Herman Geuvers	(In)consistency of Extensions of Higher Order Logic and Type Theory.	TYPES	2006	DBLP DOI BibTeX RDF
27	Brigitte Pientka	Termination and Reduction Checking for Higher-Order Logic Programs.	IJCAR	2001	DBLP DOI BibTeX RDF
26	Douglas J. Howe	Higher-order abstract syntax in classical higher-order logic.	LFMTP	2009	DBLP DOI BibTeX RDF
26	Allen Van Gelder, Geoff Sutcliffe	Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation.	IJCAR	2006	DBLP DOI BibTeX RDF
26	Martin Hofmann 0001, Donald Sannella	On Behavioral Abstraction and Behavioural Satisfaction in Higher-Order Logic.	TAPSOFT	1995	DBLP DOI BibTeX RDF
26	Konstantine Arkoudas, Selmer Bringsjord	Metareasoning for Multi-agent Epistemic Logics.	CLIMA	2004	DBLP DOI BibTeX RDF
25	James Lipton, Susana Nieva	Higher-Order Logic Programming Languages with Constraints: A Semantics.	TLCA	2007	DBLP DOI BibTeX RDF
25	Steven Obua	Checking Conservativity of Overloaded Definitions in Higher-Order Logic.	RTA	2006	DBLP DOI BibTeX RDF
25	James H. Andrews	Executing Formal Specifications by Translation to Higher Order Logic Programming.	TPHOLs	1997	DBLP DOI BibTeX RDF
25	Alain Hui-Bon-Hoa	A Bottom-Up Interpreter for a Higher-Order Logic Programming Language.	PLILP	1992	DBLP DOI BibTeX RDF
25	Matt Fairtlough, Michael Mendler, Xiaochun Cheng	Abstraction and Refinement in Higher Order Logic.	TPHOLs	2001	DBLP DOI BibTeX RDF
25	Rafael del Vado Vírseda	A higher-order logical framework for the algorithmic debugging and verification of declarative programs.	PPDP	2009	DBLP DOI BibTeX RDF	algorithmic debugging, declarative verification, multiparadigm declarative programming, lambda calculus
24	Norbert Völker	HOL2P - A System of Classical Higher Order Logic with Second Order Polymorphism.	TPHOLs	2007	DBLP DOI BibTeX RDF
24	Farhad Mehta, Tobias Nipkow	Proving Pointer Programs in Higher-Order Logic.	CADE	2003	DBLP DOI BibTeX RDF
24	Zachary Snow, David Baelde, Gopalan Nadathur	A meta-programming approach to realizing dependently typed logic programming.	PPDP	2010	DBLP DOI BibTeX RDF	dependently typed lambda calculi, higher-order logic programming, translation, logical frameworks
24	Jasmin Christian Blanchette	Proof Pearl: Mechanizing the Textbook Proof of Huffman's Algorithm.	J. Autom. Reason.	2009	DBLP DOI BibTeX RDF	Interactive theorem provers, Huffman coding, Higher-order logic
24	Silvio Ghilardi, Enrica Nicolini, Daniele Zucchelli	A comprehensive combination framework.	ACM Trans. Comput. Log.	2008	DBLP DOI BibTeX RDF	modal and description logics, decision procedures, Combination, higher-order logic, satisfiability modulo theory
24	Osman Hasan, Sofiène Tahar	Using Theorem Proving to Verify Expectation and Variance for Discrete Random Variables.	J. Autom. Reason.	2008	DBLP DOI BibTeX RDF	Coupon collector’s problem, Probabilistic analysis, Higher-order-logic, Probability theory, Statistical properties, HOL theorem prover
24	David R. Lester	Real Number Calculations and Theorem Proving.	TPHOLs	2008	DBLP DOI BibTeX RDF	Computable Reals, Exact Arithmetic, Theorem Proving, PVS, Higher-order Logic
24	Murdoch Gabbay, Aad Mathijssen	One-and-a-halfth-order logic.	PPDP	2006	DBLP DOI BibTeX RDF	?-conversion, Fraenkel-Mostowski techniques, meta-variables, nominal terms, first-order logic, higher-order logic
24	Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith 0008, Keith Wansbrough	Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and sockets.	SIGCOMM	2005	DBLP DOI BibTeX RDF	specification, TCP/IP, network protocols, operational semantics, API, conformance testing, higher-order logic, sockets, HOL
24	Skander Kort, Sofiène Tahar, Paul Curzon	Hierarchical formal verification using a hybrid tool.	Int. J. Softw. Tools Technol. Transf.	2003	DBLP DOI BibTeX RDF	HOL (higher-order logic), MDG (multiway decision graphs), Hybrid tools, Hierarchical verification
24	Gilles Dowek, Thérèse Hardin, Claude Kirchner	Theorem Proving Modulo.	J. Autom. Reason.	2003	DBLP DOI BibTeX RDF	sequent calculus modulo, resolution, rewriting, automated theorem proving, higher-order logic, cut elimination, narrowing, Skolemization, deduction modulo
24	Monica Nesi	Formalising a Value-Passing Calculus in HOL.	Formal Aspects Comput.	1999	DBLP DOI BibTeX RDF	Meta-theoretic reasoning, Formal verification, Theorem proving, Higher order logic, Process calculi
24	Koichi Takahashi, Masami Hagiya	Proving as Editing HOL Tactics.	Formal Aspects Comput.	1999	DBLP DOI BibTeX RDF	Tactic-Based Theorem Prover, User interface, Higher Order Logic, Emacs
24	Axel Dold, Friedrich W. von Henke, Holger Pfeifer, Harald Rueß	Formal Verification of Transformations for Peephole Optimization.	FME	1997	DBLP DOI BibTeX RDF	reusability of specifications, formal verification, transformations, higher-order logic
24	John Esch	Contexts, Canons and Coreferent Types.	ICCS	1994	DBLP DOI BibTeX RDF	Context, Concept, Conceptual Graph, Higher Order Logic, Canon
24	George W. Ernst	A Definition-Driven Theorem Prover.	IEEE Trans. Computers	1976	DBLP DOI BibTeX RDF	natural deduction systems, Artificial intelligence, heuristic search, higher order logic, mechanical theorem proving
24	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
24	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
24	Sten Agerholm, Michael J. C. Gordon	Experiments with ZF Set Theory in HOL and Isabelle.	TPHOLs	1995	DBLP DOI BibTeX RDF
23	Herman Geuvers, Gueorgui I. Jojgov	Open Proofs and Open Terms: A Basis for Interactive Logic.	CSL	2002	DBLP DOI BibTeX RDF	open terms, meta-variables, formulas-as-types, type theory, interactive theorem proving
23	Tomasz Pietrzykowski	A Complete Mechanization of Second-Order Type Theory.	J. ACM	1973	DBLP DOI BibTeX RDF
23	Amy P. Felty	Proof Search with Set Variable Instantiation in the Calculus of Constructions.	CADE	1996	DBLP DOI BibTeX RDF
23	Brigitte Pientka	Verifying Termination and Reduction Properties about Higher-Order Logic Programs.	J. Autom. Reason.	2005	DBLP DOI BibTeX RDF	termination, Logical frameworks
22	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
22	Serge Autexier	On the Dynamic Increase of Multiplicities in Matrix Proof Methods for Classical Higher-Order Logic.	TABLEAUX	2005	DBLP DOI BibTeX RDF
22	Marco Benini, Sara Kalvala, Dirk Nowotka	Program Abstraction in a Higher-Order Logic Framework.	TPHOLs	1998	DBLP DOI BibTeX RDF
22	Weidong Chen 0005, David Scott Warren	Compilation of Predicate Abstractions in Higher-Order Logic Programming.	PLILP	1991	DBLP DOI BibTeX RDF
22	Joseph A. Goguen, Rod M. Burstall	Institutions: Abstract Model Theory for Specification and Programming.	J. ACM	1992	DBLP DOI BibTeX RDF
21	Lauri Hella, Jose Maria Turull Torres	Complete Problems for Higher Order Logics.	CSL	2006	DBLP DOI BibTeX RDF	Lindström Quantifiers, Complete Problems, Higher Order Logics
21	Helmut Schwichtenberg	Proof Search in Minimal Logic.	AISC	2004	DBLP DOI BibTeX RDF
21	Christoph Benzmüller, Florian Rabe 0001, Geoff Sutcliffe	THF0 - The Core of the TPTP Language for Higher-Order Logic.	IJCAR	2008	DBLP DOI BibTeX RDF
21	Oliver Pell	Verification of FPGA Layout Generators in Higher-Order Logic.	J. Autom. Reason.	2006	DBLP DOI BibTeX RDF	layout description, circuit verification, FPGA, theorem proving
21	Konrad Slind	AC Unification in HOL90.	HUG	1993	DBLP DOI BibTeX RDF
21	Peter B. Andrews	Connections and Higher-Order Logic.	CADE	1986	DBLP DOI BibTeX RDF