Results
Found 681 publication records. Showing 681 according to the selection in the facets
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 |
|
Displaying result #1 - #100 of 681 (100 per page; Change: ) Pages: [ 1][ 2][ 3][ 4][ 5][ 6][ 7][ >>] |