Search results for "Higher-order-logic"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
15	Dale Miller 0001, Gopalan Nadathur	Higher-Order Logic Programming.	ICLP	1986	DBLP DOI BibTeX RDF
15	Dale Miller 0001, Gopalan Nadathur	Some Uses of Higher-Order Logic in Computational Linguistics.	ACL	1986	DBLP BibTeX RDF
15	Christian Hort, Horst Osswald	On Nonstandard Models in Higher Order Logic.	J. Symb. Log.	1984	DBLP DOI BibTeX RDF
15	Dag Prawitz	Hauptsatz for Higher Order Logic.	J. Symb. Log.	1968	DBLP DOI BibTeX RDF
15	John Harrison 0001	Theorem Proving for Verification (Invited Tutorial).	CAV	2008	DBLP DOI BibTeX RDF
15	Qing Liu 0011, Hui Sun	Theoretical Study of Granular Computing.	RSKT	2006	DBLP DOI BibTeX RDF	Granular logic, closeness degree, granular computing
14	Konrad Slind, Scott Owens, Juliano Iyoda, Mike Gordon	Proof producing synthesis of arithmetic and cryptographic hardware.	Formal Aspects Comput.	2007	DBLP DOI BibTeX RDF	Cryptography, Compiling, Theorem proving, Hardware synthesis, High assurance
14	Nita Goyal, Charles Hoch, Ravi Krishnamurthy, Brian Meckler, Michael Suckow	Is GUI Programming a Database Research Problem?	SIGMOD Conference	1996	DBLP DOI BibTeX RDF
14	Shiu-Kai Chin, Edward P. Stabler	Synthesis of arithmetic hardware using hardware metafunctions.	IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.	1990	DBLP DOI BibTeX RDF
13	Peter V. Homeier	The HOL-Omega Logic.	TPHOLs	2009	DBLP DOI BibTeX RDF
13	M. Randall Holmes	A Strong and Mechanizable Grand Logic.	TPHOLs	2000	DBLP DOI BibTeX RDF
13	Peter V. Homeier	A Design Structure for Higher Order Quotients.	TPHOLs	2005	DBLP DOI BibTeX RDF
13	Shiu-Kai Chin	Verified functions for generating signed-binary arithmetic hardware.	IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.	1992	DBLP DOI BibTeX RDF
12	Tobias Nipkow, Lawrence C. Paulson	Isabelle-91.	CADE	1992	DBLP DOI BibTeX RDF
12	Jean Goubault-Larrecq	Ramified Higher-Order Unification.	LICS	1997	DBLP DOI BibTeX RDF
12	David A. Basin	The Next 700 Synthesis Calculi.	FME	2002	DBLP DOI BibTeX RDF
11	David Hemer	Specification-Based Retrieval Strategies for Component Architectures.	Australian Software Engineering Conference	2005	DBLP DOI BibTeX RDF
11	Susumu Nishimura	Safe Modification of Pointer Programs in Refinement Calculus.	MPC	2008	DBLP DOI BibTeX RDF
11	Ramsay Taylor	Separation of Z Operations.	ABZ	2008	DBLP DOI BibTeX RDF
11	Thumrongsak Kosiyatrakul, Susan Older, Shiu-Kai Chin	A Modal Logic for Role-Based Access Control.	MMM-ACNS	2005	DBLP DOI BibTeX RDF
11	Aaron Stump	Subset Types and Partial Functions.	CADE	2003	DBLP DOI BibTeX RDF
11	Bart Jacobs 0001, Erik Poll	A Logic for the Java Modeling Language JML.	FASE	2001	DBLP DOI BibTeX RDF
11	Andrew W. Appel, Edward W. Felten	Proof-Carrying Authentication.	CCS	1999	DBLP DOI BibTeX RDF
10	Daniel Leivant	The Functions Provable by First Order Abstraction.	LPAR	2001	DBLP DOI BibTeX RDF
10	Gilles Dowek, Benjamin Werner	Proof Normalization Modulo.	TYPES	1998	DBLP DOI BibTeX RDF
10	Yann Régis-Gianas, François Pottier	A Hoare Logic for Call-by-Value Functional Programs.	MPC	2008	DBLP DOI BibTeX RDF
10	Aleksandar Nanevski, Amal Ahmed 0001, Greg Morrisett, Lars Birkedal	Abstract Predicates and Mutable ADTs in Hoare Type Theory.	ESOP	2007	DBLP DOI BibTeX RDF
10	Behzad Akbarpour, Sofiène Tahar	An approach for the formal verification of DSP designs using Theorem proving.	IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.	2006	DBLP DOI BibTeX RDF
10	Christoph Benzmüller, Chad E. Brown	A Structured Set of Higher-Order Problems.	TPHOLs	2005	DBLP DOI BibTeX RDF
10	David A. Basin, Hironobu Kuruma, Kazuo Takaragi, Burkhart Wolff	Verification of a Signature Architecture with HOL-Z.	FM	2005	DBLP DOI BibTeX RDF
10	Sava Krstic, John Matthews	Semantics of the reFLect language.	PPDP	2004	DBLP DOI BibTeX RDF
10	Lutz Schröder	The Logic of the Partial lambda-Calculus with Equality.	CSL	2004	DBLP DOI BibTeX RDF
10	Sava Krstic, John Matthews	Inductive Invariants for Nested Recursion.	TPHOLs	2003	DBLP DOI BibTeX RDF
10	Nancy A. Day, Jeffrey J. Joyce	A Framework for Multi-Notation Requirements Specification and Analysis.	ICRE	2000	DBLP DOI BibTeX RDF
10	David Lacey, Julian Richardson, Alan Smaill	Logic Program Synthesis in a Higher-Order Setting.	Computational Logic	2000	DBLP DOI BibTeX RDF
10	Nancy A. Day, Jeffrey J. Joyce	Symbolic Functional Evaluation.	TPHOLs	1999	DBLP DOI BibTeX RDF
10	Dan Zhou, Joncheng C. Kuo, Susan Older, Shiu-Kai Chin	Formal Development of Secure Email.	HICSS	1999	DBLP DOI BibTeX RDF	high-assurance design and synthesis, secure email systems, formal methods, component-based design
10	Ulrich Hensel, Marieke Huisman, Bart Jacobs 0001, Hendrik Tews	Reasonong about Classess in Object-Oriented Languages: Logical Models and Tools.	ESOP	1998	DBLP DOI BibTeX RDF
10	Peter B. Andrews, Chad E. Brown, Frank Pfenning, Matthew Bishop, Sunil Issar, Hongwei Xi	ETPS: A System to Help Students Write Formal Proofs.	J. Autom. Reason.	2004	DBLP DOI BibTeX RDF	ETPS, GRADER, teaching logic, education, proofs
10	Till Mossakowski	Heterogeneous Development Graphs and Heterogeneous Borrowing.	FoSSaCS	2002	DBLP DOI BibTeX RDF
9	Magnus O. Myreen, Michael J. C. Gordon	Hoare Logic for Realistically Modelled Machine Code.	TACAS	2007	DBLP DOI BibTeX RDF
9	Sen Xiang, Yiyun Chen, Chunxiao Lin, Long Li	Modularly Certified Dynamic Storage Allocation in SCAP.	QSIC	2006	DBLP DOI BibTeX RDF
9	Olha Shkaravska	Types with semantics: soundness proof assistant.	MERLIN	2005	DBLP DOI BibTeX RDF	type system, assertion, automated theorem proving, program logic
9	Arnd Poetzsch-Heffter, Peter Müller 0001	A Programming Logic for Sequential Java.	ESOP	1999	DBLP DOI BibTeX RDF
9	F. Keith Hanna, Neil Daeche	Purely Functional Implementation of a Logic.	CADE	1986	DBLP DOI BibTeX RDF
9	Steve M. Shaner, Gary T. Leavens, David A. Naumann	Modular verification of higher-order methods with mandatory calls specified by model programs.	OOPSLA	2007	DBLP DOI BibTeX RDF	grey-box approach, higher order method, mandatory call, model program, verification, specification languages, hoare logic, refinement calculus
9	Alberto Momigliano, Frank Pfenning	Higher-order pattern complement and the strict lambda-calculus.	ACM Trans. Comput. Log.	2003	DBLP DOI BibTeX RDF	higher-order patterns, strict ?-calculus, Complement
8	Anna Mikhajlova, Joakim von Wright	Proving Isomorphism of First-Order Logic Proof Systems in HOL.	TPHOLs	1998	DBLP DOI BibTeX RDF
8	Amy P. Felty, Alberto Momigliano	Reasoning with hypothetical judgments and open terms in hybrid.	PPDP	2009	DBLP DOI BibTeX RDF	name-binding, induction, logical frameworks, higher-order abstract syntax, interactive theorem proving
8	Susmit Sarkar, Brigitte Pientka, Karl Crary	Small Proof Witnesses for LF.	ICLP	2005	DBLP DOI BibTeX RDF
8	Lee Pike, Jeffrey Maddalon, Paul S. Miner, Alfons Geser	Abstractions for Fault-Tolerant Distributed System Verification.	TPHOLs	2004	DBLP DOI BibTeX RDF
8	Shin-ya Katsumata	Behavioural Equivalence and Indistinguishability in Higher-Order Typed Languages.	WADT	2002	DBLP DOI BibTeX RDF
8	Chad E. Brown	Solving for Set Variables in Higher-Order Theorem Proving.	CADE	2002	DBLP DOI BibTeX RDF
8	James Reynolds	Automatically Translating Type and Function Definitions from HOL to ACL2.	TPHOLs	2007	DBLP DOI BibTeX RDF
8	Charles Bouillaguet, Viktor Kuncak, Thomas Wies, Karen Zee, Martin C. Rinard	Using First-Order Theorem Provers in the Jahob Data Structure Verification System.	VMCAI	2007	DBLP DOI BibTeX RDF
8	Dieter Spreen	A New Model Construction for the Polymorphic Lambda Calculus.	LPAR	2000	DBLP DOI BibTeX RDF
8	Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Erica Melis, Dan Nesmith, Jörn Richts, Jörg H. Siekmann	KEIM: A Toolkit for Automated Deduction.	CADE	1994	DBLP DOI BibTeX RDF
7	Sylvia B. Encheva, Sharil Tumin	On Drawing Conclusions in Presence of Inconsistent Data.	KES-AMSTA	2008	DBLP DOI BibTeX RDF	five-valued logic, automated tests
7	Sylvia B. Encheva, Sharil Tumin	Management of Inconsistent Data.	OTM Workshops (2)	2007	DBLP DOI BibTeX RDF	five-valued logic, automated tests
7	Ondrej Rysavý, Frantisek Bures	Formal Abstract Architecture for Use Case Specifications.	ECBS	2004	DBLP DOI BibTeX RDF
7	Harvey Tuch	Formal Verification of C Systems Code.	J. Autom. Reason.	2009	DBLP DOI BibTeX RDF	C, Separation logic, Interactive theorem proving
7	Kee Siong Ng, John W. Lloyd, William T. B. Uther	Probabilistic modelling, inference and learning using logical theories.	Ann. Math. Artif. Intell.	2008	DBLP DOI BibTeX RDF	Mathematics Subject Classifications (2000) 03B15, 03B48, 68T37
7	Achim D. Brucker, Burkhart Wolff	An Extensible Encoding of Object-oriented Data Models in hol.	J. Autom. Reason.	2008	DBLP DOI BibTeX RDF	Verification, Theorem proving, Object-oriented data models, hol
7	Anduo Wang, Fei He 0001, Ming Gu 0001, Xiaoyu Song	Verifying Java Programs By Theorem Prover HOL.	COMPSAC (1)	2006	DBLP DOI BibTeX RDF
7	Robert L. Constable, Wojciech Moczydlowski	Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics.	IJCAR	2006	DBLP DOI BibTeX RDF
7	Thomas Tuerk, Klaus Schneider 0001, Mike Gordon	Model Checking PSL Using HOL and SMV.	Haifa Verification Conference	2006	DBLP DOI BibTeX RDF
7	Carl-Johan H. Seger, Robert B. Jones, John W. O'Leary, Thomas F. Melham, Mark D. Aagaard, Clark W. Barrett, Don Syme	An industrially effective environment for formal hardware verification.	IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.	2005	DBLP DOI BibTeX RDF
7	Jens Brandt 0001, Klaus Schneider 0001	Using Three-Valued Logic to Specify and Verify Algorithms of Computational Geometry.	ICFEM	2005	DBLP DOI BibTeX RDF
7	John W. Lloyd, Tim D. Sears	An Architecture for Rational Agents.	DALT	2005	DBLP DOI BibTeX RDF
7	Stefan Berghofer	Extracting a Normalization Algorithm in Isabelle/HOL.	TYPES	2004	DBLP DOI BibTeX RDF
7	Behzad Akbarpour, Sofiène Tahar	The Application of Formal Verification to SPW Designs.	DSD	2003	DBLP DOI BibTeX RDF
7	Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom, Konrad Slind	Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT.	CHARME	2003	DBLP DOI BibTeX RDF
7	Till Mossakowski, Horst Reichel, Markus Roggenbach, Lutz Schröder	Algebraic-Coalgebraic Specification in Co Casl.	WADT	2002	DBLP DOI BibTeX RDF
7	John W. Lloyd	Learning Comprehensible Theories from Structured Data.	Machine Learning Summer School	2002	DBLP DOI BibTeX RDF
7	George C. Necula, Shree Prakash Rahul	Oracle-based checking of untrusted software.	POPL	2001	DBLP DOI BibTeX RDF	ORACLE
7	Andrew W. Appel, Amy P. Felty	A Semantic Model of Types and Machine Instructions for Proof-Carrying Code.	POPL	2000	DBLP DOI BibTeX RDF
7	Dan Zhou, Shiu-Kai Chin	Formal Analysis of a Secure Communication Channel: Secure Core-Email Protocol.	World Congress on Formal Methods	1999	DBLP DOI BibTeX RDF
7	Mark D. Aagaard, Thomas F. Melham, John W. O'Leary	Xs are for Trajectory Evaluation, Booleans are for Theorem Proving.	CHARME	1999	DBLP DOI BibTeX RDF
7	W. O. David Griffioen, Marieke Huisman	A Comparison of PVS and Isabelle/HOL.	TPHOLs	1998	DBLP DOI BibTeX RDF
7	Florian Kammüller	Modular Structures as Dependent Types in Isabelle.	TYPES	1998	DBLP DOI BibTeX RDF
7	Shiu-Kai Chin, Jang Dae Kim	An Instruction Set Process Calculus.	FMCAD	1998	DBLP DOI BibTeX RDF
7	Michael C. McFarland	Formal verification of sequential hardware: a tutorial.	IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.	1993	DBLP DOI BibTeX RDF
7	Lawrence C. Paulson	A formulation of the simple theory of types (for Isabelle).	Conference on Computer Logic	1988	DBLP DOI BibTeX RDF
6	Osman Hasan, Sanaz Khan Afshar, Sofiène Tahar	Formal Analysis of Optical Waveguides in HOL.	TPHOLs	2009	DBLP DOI BibTeX RDF
6	Ganesh Gopalakrishnan, Yue Yang, Hemanthkumar Sivaraj	QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings.	CAV	2004	DBLP DOI BibTeX RDF
6	Lawrence C. Paulson	Inductive Analysis of the Internet Protocol TLS (Position Paper).	Security Protocols Workshop	1998	DBLP DOI BibTeX RDF
6	Osman Hasan, Naeem Abbasi, Behzad Akbarpour, Sofiène Tahar, Reza Akbarpour	Formal Reasoning about Expectation Properties for Continuous Random Variables.	FM	2009	DBLP DOI BibTeX RDF
6	Karen Zee, Viktor Kuncak, Martin C. Rinard	Full functional verification of linked data structures.	PLDI	2008	DBLP DOI BibTeX RDF	java, verification, data structure, decision procedure, theorem prover
6	Amine Chaieb	Verifying Mixed Real-Integer Quantifier Elimination.	IJCAR	2006	DBLP DOI BibTeX RDF
6	Behzad Akbarpour, Sofiène Tahar	Error Analysis of Digital Filters Using Theorem Proving.	TPHOLs	2004	DBLP DOI BibTeX RDF
6	René MacKinney-Romero, Christophe G. Giraud-Carrier	Inducing Classification Rules from Highly-Structured Data with Composition.	MICAI	2004	DBLP DOI BibTeX RDF
6	Joe Hurd	An LCF-Style Interface between HOL and First-Order Logic.	CADE	2002	DBLP DOI BibTeX RDF
6	Gavin J. Doherty, José Creissac Campos, Michael D. Harrison	Representational Reasoning and Verification.	Formal Aspects Comput.	2000	DBLP DOI BibTeX RDF	Human-computer interaction, Verification, Formal specification, Representation, Distributed cognition
6	V. K. Pisini, Sofiène Tahar, Paul Curzon, Otmane Aït Mohamed, Xiaoyu Song	Formal hardware verification by integrating HOL and MDG.	ACM Great Lakes Symposium on VLSI	2000	DBLP DOI BibTeX RDF
6	Pierre Chartier	Formalisation of B in Isabelle/HOL.	B	1998	DBLP DOI BibTeX RDF
5	John Harrison 0001	HOL Light: An Overview.	TPHOLs	2009	DBLP DOI BibTeX RDF
5	Tom Ridge	Verifying distributed systems: the operational approach.	POPL	2009	DBLP DOI BibTeX RDF	ground and symbolic evaluation, hoare-style assertions, persistent queue, rely/guarantee, distributed, refinement, invariants, network protocol, operational semantics, infrastructure, separation, linearizability, hol, ocaml, local reasoning, inductive reasoning
5	Erik Schierboom, Alejandro Tamalet, Hendrik Tews, Marko C. J. D. van Eekelen, Sjaak Smetsers	Preemption Abstraction.	FMICS	2009	DBLP DOI BibTeX RDF
5	Osman Hasan, Naeem Abbasi, Sofiène Tahar	Formal Probabilistic Analysis of Stuck-at Faults in Reconfigurable Memory Arrays.	IFM	2009	DBLP DOI BibTeX RDF
5	Ralf Lämmel	Scrap your boilerplate: prologically!	PPDP	2009	DBLP DOI BibTeX RDF	scrap your boilerplate, prolog, haskell, stratego