Search results for "HOL"

Hits ?▲	Authors	Title	Venue	Year	Link
16	Yutaka Nagashima, Yilun He	PaMpeR: proof method recommendation system for Isabelle/HOL.	ASE	2018	DBLP DOI BibTeX RDF
16	Christoph Benzmüller, Ali Farjami, Xavier Parent	A Dyadic Deontic Logic in HOL.	DEON	2018	DBLP BibTeX RDF
16	Alexander Maletzky, Fabian Immler	Gröbner Bases of Modules and Faugère's F4 Algorithm in Isabelle/HOL.	CICM	2018	DBLP DOI BibTeX RDF
16	Yutaka Nagashima, Julian Parsert	Goal-Oriented Conjecturing for Isabelle/HOL.	CICM	2018	DBLP DOI BibTeX RDF
16	Roberto Peñaranda, Crispín Gómez Requena, María Engracia Gómez, Pedro López 0001	XOR-based HoL-blocking reduction routing mechanisms for direct networks.	Parallel Comput.	2017	DBLP DOI BibTeX RDF
16	Adnan Rashid, Osman Hasan	Formalization of Transform Methods using HOL Light.	CoRR	2017	DBLP BibTeX RDF
16	Ben Blumson	Anselm's God in Isabelle/HOL.	Arch. Formal Proofs	2017	DBLP BibTeX RDF
16	Daniel Kirchner	Representation and Partial Automation of the Principia Logico-Metaphysica in Isabelle/HOL.	Arch. Formal Proofs	2017	DBLP BibTeX RDF
16	Andreas Lochbihler, S. Reza Sefidgar, Bhargav Bhatt	Game-based cryptography in HOL.	Arch. Formal Proofs	2017	DBLP BibTeX RDF
16	David Fuenmayor, Christoph Benzmüller	Types, Tableaus and Gödel's God in Isabelle/HOL.	Arch. Formal Proofs	2017	DBLP BibTeX RDF
16	Jesús Aransay, Jose Divasón	A Formalisation in HOL of the Fundamental Theorem of Linear Algebra and Its Application to the Solution of the Least Squares Problem.	J. Autom. Reason.	2017	DBLP DOI BibTeX RDF
16	Johannes Hölzl	Markov Chains and Markov Decision Processes in Isabelle/HOL.	J. Autom. Reason.	2017	DBLP DOI BibTeX RDF
16	Manuel Eberl	Proving Divide and Conquer Complexities in Isabelle/HOL.	J. Autom. Reason.	2017	DBLP DOI BibTeX RDF
16	Pedro Yébenes, Jesús Escudero-Sahuquillo, Pedro Javier García, Francisco J. Quiles 0001, Torsten Hoefler	An Effective Queuing Scheme to Provide Slim Fly Topologies with HoL Blocking Reduction and Deadlock Freedom for Minimal-Path Routing.	HiPINEB@HPCA	2017	DBLP DOI BibTeX RDF
16	Andreas Viktor Hess, Sebastian Mödersheim	Formalizing and Proving a Typing Result for Security Protocols in Isabelle/HOL.	CSF	2017	DBLP DOI BibTeX RDF
16	Simon Foster 0001, Jim Woodcock 0001	Towards Verification of Cyber-Physical Systems with UTP and Isabelle/HOL.	Concurrency, Security, and Puzzles	2017	DBLP DOI BibTeX RDF
16	Ondrej Kuncar, Andrei Popescu 0001	Comprehending Isabelle/HOL's Consistency.	ESOP	2017	DBLP DOI BibTeX RDF
16	Yutaka Nagashima, Ramana Kumar	A Proof Strategy Language and Proof Script Generation for Isabelle/HOL.	CADE	2017	DBLP DOI BibTeX RDF
16	Albert Rizaldi, Jonas Keinholz, Monika Huber 0001, Jochen Feldle, Fabian Immler, Matthias Althoff, Eric Hilgendorf, Tobias Nipkow	Formalising and Monitoring Traffic Rules for Autonomous Vehicles in Isabelle/HOL.	IFM	2017	DBLP DOI BibTeX RDF
16	Sven Linker	Spatial Reasoning About Motorway Traffic Safety with Isabelle/HOL.	IFM	2017	DBLP DOI BibTeX RDF
16	Said Meghzili, Allaoua Chaoui, Martin Strecker, Elhillali Kerkouche	On the Verification of UML State Machine Diagrams to Colored Petri Nets Transformation Using Isabelle/HOL.	IRI	2017	DBLP DOI BibTeX RDF
16	Ghassen Helali, Sofiène Tahar, Osman Hasan, Tsvetan Dunchev	Formal Analysis of Information Flow in HOL.	SETTA	2017	DBLP DOI BibTeX RDF
16	Johannes Hölzl	Markov processes in Isabelle/HOL.	CPP	2017	DBLP DOI BibTeX RDF
16	Lawrence C. Paulson	Porting the HOL light analysis library: some lessons (invited talk).	CPP	2017	DBLP DOI BibTeX RDF
16	Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel	Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL.	FSCD	2017	DBLP DOI BibTeX RDF
16	Joseph R. Harrison	Towards an Isabelle/HOL formalisation of core Erlang.	Erlang Workshop	2017	DBLP DOI BibTeX RDF
16	Adnan Rashid, Osman Hasan	Formalization of Transform Methods Using HOL Light.	CICM	2017	DBLP DOI BibTeX RDF
16	Pedro Yébenes, Jesús Escudero-Sahuquillo, Pedro Javier García, Francisco J. Quiles 0001	Straightforward solutions to reduce HoL blocking in different Dragonfly fully-connected interconnection patterns.	J. Supercomput.	2016	DBLP DOI BibTeX RDF
16	Nikolaos Chrysos, Lydia Y. Chen, Christoforos Kachris, Manolis Katevenis	Discharging the Network From Its Flow Control Headaches: Packet Drops and HOL Blocking.	IEEE/ACM Trans. Netw.	2016	DBLP DOI BibTeX RDF
16	Samy Bakheet, Ayoub Al-Hamadi	A Discriminative Framework for Action Recognition Using f-HOL Features.	Inf.	2016	DBLP DOI BibTeX RDF
16	Mario Carneiro	Conversion of HOL Light proofs into Metamath.	J. Formaliz. Reason.	2016	DBLP DOI BibTeX RDF
16	Lars Hupel, Viktor Kuncak	Translating Scala Programs to Isabelle/HOL.	CoRR	2016	DBLP BibTeX RDF
16	Christian Sternagel, Thomas Sternagel	Level-Confluence of 3-CTRSs in Isabelle/HOL.	CoRR	2016	DBLP BibTeX RDF
16	Rob Arthan	On Definitions of Constants and Types in HOL.	J. Autom. Reason.	2016	DBLP DOI BibTeX RDF
16	Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, Josef Urban	A Learning-Based Fact Selector for Isabelle/HOL.	J. Autom. Reason.	2016	DBLP DOI BibTeX RDF
16	Umair Siddique, Sofiène Tahar	On the formal analysis of Gaussian optical systems in HOL.	Formal Aspects Comput.	2016	DBLP DOI BibTeX RDF
16	Jesús Aransay, Jose Divasón	Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL.	Formal Aspects Comput.	2016	DBLP DOI BibTeX RDF
16	Christoph Benzmüller, Dana S. Scott	Automating Free Logic in Isabelle/HOL.	ICMS	2016	DBLP DOI BibTeX RDF
16	Alexander Steen, Max Wisniewski, Christoph Benzmüller	Agent-Based HOL Reasoning.	ICMS	2016	DBLP DOI BibTeX RDF
16	Max Wisniewski, Alexander Steen, Kim Kern, Christoph Benzmüller	Effective Normalization Techniques for HOL.	IJCAR	2016	DBLP DOI BibTeX RDF
16	Lars Hupel, Viktor Kuncak	Translating Scala Programs to Isabelle/HOL - System Description.	IJCAR	2016	DBLP DOI BibTeX RDF
16	René Thiemann, Akihisa Yamada 0002	Algebraic Numbers in Isabelle/HOL.	ITP	2016	DBLP DOI BibTeX RDF
16	Mohammad Abdulaziz, Lawrence C. Paulson	An Isabelle/HOL Formalisation of Green's Theorem.	ITP	2016	DBLP DOI BibTeX RDF
16	Mark Adams	HOL Zero's Solutions for Pollack-Inconsistency.	ITP	2016	DBLP DOI BibTeX RDF
16	René Thiemann, Akihisa Yamada 0002	Formalizing jordan normal forms in Isabelle/HOL.	CPP	2016	DBLP DOI BibTeX RDF
16	Alexander Steen, Max Wisniewski, Christoph Benzmüller	Tutorial on Reasoning in Expressive Non-Classical Logics with Isabelle/HOL.	GCAI	2016	DBLP DOI BibTeX RDF
16	Xiaojun Ji, Lihua Song	Mutual Exclusion Verification of Peterson's Solution in Isabelle/HOL.	TSA	2016	DBLP DOI BibTeX RDF
16	Cvetan Dunchev, Claudio Sacerdoti Coen, Enrico Tassi	Implementing HOL in an Higher Order Logic Programming Language.	LFMTP	2016	DBLP DOI BibTeX RDF
16	Muhammad Qasim, Osman Hasan, Maissa Elleuch, Sofiène Tahar	Formalization of Normal Random Variables in HOL.	CICM	2016	DBLP DOI BibTeX RDF
16	Charles Jacobsen, Alexey Solovyev, Ganesh Gopalakrishnan	A Parameterized Floating-Point Formalizaton in HOL Light.	NSV	2015	DBLP DOI BibTeX RDF
16	Crispín Gómez Requena, Francisco Gilabert Villamón, María Engracia Gómez, Pedro López 0001, José Duato	A HoL-blocking aware mechanism for selecting the upward path in fat-tree topologies.	J. Supercomput.	2015	DBLP DOI BibTeX RDF
16	Mark Adams	The Common HOL Platform.	PxTP@CADE	2015	DBLP DOI BibTeX RDF
16	Ali Assaf 0002, Raphaël Cauderlier	Mixing HOL and Coq in Dedukti (Extended Abstract).	PxTP@CADE	2015	DBLP DOI BibTeX RDF
16	Wenda Li, Grant Olney Passmore, Lawrence C. Paulson	A Complete Decision Procedure for Univariate Polynomial Problems in Isabelle/HOL.	CoRR	2015	DBLP BibTeX RDF
16	Ali Assaf 0002, Guillaume Burel	Translating HOL to Dedukti.	PxTP@CADE	2015	DBLP DOI BibTeX RDF
16	Christoph Benzmüller, Maximilian Claus, Nik Sultana	Systematic Verification of the Modal Logic Cube in Isabelle/HOL.	PxTP@CADE	2015	DBLP DOI BibTeX RDF
16	Thibault Gauthier, Cezary Kaliszyk	Sharing HOL4 and HOL Light proof knowledge.	CoRR	2015	DBLP BibTeX RDF
16	Abderrahmane Feliachi, Marie-Claude Gaudel, Burkhart Wolff	Symbolic Test-generation in HOL-TESTGEN/CirTA A Case Study.	Int. J. Softw. Informatics	2015	DBLP BibTeX RDF
16	René Thiemann, Akihisa Yamada 0002	Algebraic Numbers in Isabelle/HOL.	Arch. Formal Proofs	2015	DBLP BibTeX RDF
16	Yongjian Li, Jun Pang 0001	Formalizing provable anonymity in Isabelle/HOL.	Formal Aspects Comput.	2015	DBLP DOI BibTeX RDF
16	Thibault Gauthier, Cezary Kaliszyk	Sharing HOL4 and HOL Light Proof Knowledge.	LPAR	2015	DBLP DOI BibTeX RDF
16	Roberto Peñaranda, Crispín Gómez Requena, María Engracia Gómez, Pedro López 0001	XORAdap: A HoL-Blocking Aware Adaptive Routing Algorithm.	PDP	2015	DBLP DOI BibTeX RDF
16	Alexander Schimpf, Jan-Georg Smaus	Büchi Automata Optimisations Formalised in Isabelle/HOL.	ICLA	2015	DBLP DOI BibTeX RDF
16	Waqar Ahmad, Osman Hasan, Sofiène Tahar	Formal reliability analysis of wireless sensor network data transport protocols using HOL.	WiMob	2015	DBLP DOI BibTeX RDF
16	Filip Maric, Predrag Janicic, Marko Malikovic	Proving Correctness of a KRK Chess Endgame Strategy by Using Isabelle/HOL and Z3.	CADE	2015	DBLP DOI BibTeX RDF
16	Mohamed Yousri Mahmoud, Prakash Panangaden, Sofiène Tahar	On the Formal Verification of Optical Quantum Gates in HOL.	FMICS	2015	DBLP DOI BibTeX RDF
16	Fadoua Ghourabi, Kazuko Takahashi	Formalizing the Qualitative Superposition of Rectangles in Proof Assistant Isabelle/HOL.	ICAART (2)	2015	DBLP BibTeX RDF
16	David Déharbe, Stephan Merz	Software Component Design with the B Method - A Formalization in Isabelle/HOL.	FACS	2015	DBLP DOI BibTeX RDF
16	T. V. H. Prathamesh	Formalising Knot Theory in Isabelle/HOL.	ITP	2015	DBLP DOI BibTeX RDF
16	Ondrej Kuncar, Andrei Popescu 0001	A Consistent Foundation for Isabelle/HOL.	ITP	2015	DBLP DOI BibTeX RDF
16	Christian Sternagel, René Thiemann	Deriving Comparators and Show Functions in Isabelle/HOL.	ITP	2015	DBLP DOI BibTeX RDF
16	Peter Lammich	Refinement to Imperative/HOL.	ITP	2015	DBLP DOI BibTeX RDF
16	Thomas Tuerk, Magnus O. Myreen, Ramana Kumar	Pattern Matches in HOL: - A New Representation and Improved Code Generation.	ITP	2015	DBLP DOI BibTeX RDF
16	Benja Fallenstein, Ramana Kumar	Proof-Producing Reflection for HOL - With an Application to Model Polymorphism.	ITP	2015	DBLP DOI BibTeX RDF
16	Manuel Eberl	A Decision Procedure for Univariate Real Polynomials in Isabelle/HOL.	CPP	2015	DBLP DOI BibTeX RDF
16	Cezary Kaliszyk, Josef Urban, Jirí Vyskocil	Certified Connection Tableaux Proofs for HOL Light and TPTP.	CPP	2015	DBLP DOI BibTeX RDF
16	Michael Färber 0002, Cezary Kaliszyk	Metis-based Paramodulation Tactic for HOL Light.	GCAI	2015	DBLP DOI BibTeX RDF
16	Jesús Aransay, Jose Divasón	Generalizing a Mathematical Analysis Library in Isabelle/HOL.	NFM	2015	DBLP DOI BibTeX RDF
16	Fabian Immler	Tool Presentation: Isabelle/HOL for Reachability Analysis of Continuous Systems.	ARCH@CPSWeek	2015	DBLP DOI BibTeX RDF
16	Youssef Azdoud, Aouatif Amine, Nawal Alioua, Mohammed Rziza	Pre collision detection system for pedestrian safety based on HOL.	AICCSA	2015	DBLP DOI BibTeX RDF
16	Pedro Yébenes, Jesús Escudero-Sahuquillo, Pedro Javier García, Francisco J. Quiles 0001	Efficient Queuing Schemes for HoL-Blocking Reduction in Dragonfly Topologies with Minimal-Path Routing.	CLUSTER	2015	DBLP DOI BibTeX RDF
16	Ons Seddiki, Cvetan Dunchev, Sanaz Khan Afshar, Sofiène Tahar	Enabling Symbolic and Numerical Computations in HOL Light.	CICM	2015	DBLP DOI BibTeX RDF
16	Victor Borges Ferreira Gomes	Algebraic principles for program correctness tools in Isabelle/HOL.		2015	RDF
16	Zhiping Shi 0002, Zhenke Liu, Yong Guan, Shiwei Ye, Jie Zhang 0074, Hongxing Wei	Formalization of Function Matrix Theory in HOL.	J. Appl. Math.	2014	DBLP DOI BibTeX RDF
16	Thibault Gauthier, Cezary Kaliszyk	Matching concepts across HOL libraries.	CoRR	2014	DBLP BibTeX RDF
16	Mario Carneiro	Conversion of HOL Light proofs into Metamath.	CoRR	2014	DBLP BibTeX RDF
16	Maria Spichkova	Stream processing components: Isabelle/HOL formalisation and case studies.	CoRR	2014	DBLP BibTeX RDF
16	Loïc Michel	Bernstein-based polynomial approach to study the stability of switched systems and formal verification using HOL Light.	CoRR	2014	DBLP BibTeX RDF
16	Cezary Kaliszyk, Josef Urban, Jirí Vyskocil	Certified Connection Tableaux Proofs for HOL Light and TPTP.	CoRR	2014	DBLP BibTeX RDF
16	Andreas Lochbihler, Alexandra Maximova	Stream Fusion in HOL with Code Generation.	Arch. Formal Proofs	2014	DBLP BibTeX RDF
16	Christian Sternagel, René Thiemann	Haskell's Show-Class in Isabelle/HOL.	Arch. Formal Proofs	2014	DBLP BibTeX RDF
16	Mike Stannett, István Németi	Using Isabelle/HOL to Verify First-Order Relativity Theory.	J. Autom. Reason.	2014	DBLP DOI BibTeX RDF
16	Umair Siddique, Osman Hasan	On the Formalization of Gamma Function in HOL.	J. Autom. Reason.	2014	DBLP DOI BibTeX RDF
16	Tobias Nipkow, Gerwin Klein	Concrete Semantics - With Isabelle/HOL		2014	DOI RDF
16	Alasdair Armstrong, Victor B. F. Gomes, Georg Struth	Algebras for Program Correctness in Isabelle/HOL.	RAMiCS	2014	DBLP DOI BibTeX RDF
16	Pedro Yébenes, Jesús Escudero-Sahuquillo, Crispín Gómez Requena, Pedro Javier García, Francisco J. Alfaro, Francisco J. Quiles 0001, José Duato	Combining HoL-blocking avoidance and differentiated services in high-speed interconnects.	HiPC	2014	DBLP DOI BibTeX RDF
16	Neal Master, Nicholas Bambos	Power control for wireless streaming with HOL packet deadlines.	ICC	2014	DBLP DOI BibTeX RDF
16	Roberto Peñaranda Cebrian, Crispín Gómez Requena, María Engracia Gómez Requena, Pedro Juan López Rodríguez, José Duato Marín	HoL-Blocking Avoidance Routing Algorithms in Direct Topologies.	HPCC/CSS/ICESS	2014	DBLP DOI BibTeX RDF
16	Yi Chen 0006, Xuan Wang, Lin Cai 0001	HOL delay based scheduling in wireless networks with flow-level dynamics.	GLOBECOM	2014	DBLP DOI BibTeX RDF
16	Manu K. Gupta, Nandyala Hemachandra, Jayendran Venkateswaran	On mean waiting time completeness and equivalence of EDD and HOL-PJ dynamic priority in 2-class M/G/1 queue.	VALUETOOLS	2014	DBLP DOI BibTeX RDF