Search results for "hol"

Hits ?▲	Authors	Title	Venue	Year	Link
16	Aabid Seeyal Abdul Kharim, T. V. H. Prathamesh, Shweta Rajiv, Rishi Vyas	Formalizing Free Groups in Isabelle/HOL: The Nielsen-Schreier Theorem and the Conjugacy Problem.	CICM	2023	DBLP DOI BibTeX RDF
16	Mirna Dzamonja, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson	Formalizing Ordinal Partition Relations Using Isabelle/HOL.	Exp. Math.	2022	DBLP DOI BibTeX RDF
16	Angeliki Koutsoukou-Argyraki, Wenda Li, Lawrence C. Paulson	Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL.	Exp. Math.	2022	DBLP DOI BibTeX RDF
16	Katherine Kosaian, Yong Kiam Tan, André Platzer	A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL.	CoRR	2022	DBLP DOI BibTeX RDF
16	Ciarán Dunne, J. B. Wells	Isabelle/HOL/GST: A Formal Proof Environment for Generalized Set Theories.	CoRR	2022	DBLP DOI BibTeX RDF
16	Brae J. Webb, Ian J. Hayes, Mark Utting	Verifying term graph optimizations using Isabelle/HOL.	CoRR	2022	DBLP DOI BibTeX RDF
16	Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson	Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL.	CoRR	2022	DBLP DOI BibTeX RDF
16	Yutaka Nagashima, Zijin Xu, Ningli Wang, Daniel Sebastian Goc, James Bang	Property-Based Conjecturing for Automated Induction in Isabelle/HOL.	CoRR	2022	DBLP DOI BibTeX RDF
16	Wilayat Khan, Zhe Hou, David Sanán, Jamel Nebhen, Yang Liu 0003, Alwen Tiu	An Executable Formal Model of the VHDL in Isabelle/HOL.	CoRR	2022	DBLP BibTeX RDF
16	Niels Mündler, Tobias Nipkow	A Verified Implementation of B+-Trees in Isabelle/HOL.	CoRR	2022	DBLP DOI BibTeX RDF
16	Elif Deniz, Adnan Rashid, Osman Hasan, Sofiène Tahar	On the Formalization of the Heat Conduction Problem in HOL.	CoRR	2022	DBLP DOI BibTeX RDF
16	Marco Maggesi, Cosimo Perini Brogi	A theorem prover and countermodel constructor for provability logic in HOL Light.	CoRR	2022	DBLP DOI BibTeX RDF
16	Emin Karayel	Interpolation Polynomials (in HOL-Algebra).	Arch. Formal Proofs	2022	DBLP BibTeX RDF
16	Jeffrey Ketland	Boolos's Curious Inference in Isabelle/HOL.	Arch. Formal Proofs	2022	DBLP BibTeX RDF
16	Achim D. Brucker	Nano JSON: Working with JSON formatted data in Isabelle/HOL and Isabelle/ML.	Arch. Formal Proofs	2022	DBLP BibTeX RDF
16	Christoph Benzmüller, David Fuenmayor, Alexander Steen, Geoff Sutcliffe	Automation of Boolos' Curious Inference in Isabelle/HOL.	Arch. Formal Proofs	2022	DBLP BibTeX RDF
16	Katherine Cordwell, Yong Kiam Tan, André Platzer	A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL.	Arch. Formal Proofs	2022	DBLP BibTeX RDF
16	Diego Marmsoler, Achim D. Brucker	Isabelle/Solidity: A deep Embedding of Solidity in Isabelle/HOL.	Arch. Formal Proofs	2022	DBLP BibTeX RDF
16	Sadegh Dalvandi, Brijesh Dongol, Simon Doherty, Heike Wehrheim	Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL.	J. Autom. Reason.	2022	DBLP DOI BibTeX RDF
16	Richard Schmoetten, Jake E. Palmer, Jacques D. Fleuriot	Towards Formalising Schutz' Axioms for Minkowski Spacetime in Isabelle/HOL.	J. Autom. Reason.	2022	DBLP DOI BibTeX RDF
16	Dongchen Jiang, Bo Xu	Generation of C++ Code from Isabelle/HOL Specification.	Int. J. Softw. Eng. Knowl. Eng.	2022	DBLP DOI BibTeX RDF
16	Niels Mündler, Tobias Nipkow	A Verified Implementation of B+-Trees in Isabelle/HOL.	ICTAC	2022	DBLP DOI BibTeX RDF
16	Sharar Ahmadi, Brijesh Dongol, Matt Griffin	Proving Memory Access Violations in Isabelle/HOL.	FTSCS	2022	DBLP DOI BibTeX RDF
16	Xavier Parent, Christoph Benzmüller	Automated Verification of Deontic Correspondences in Isabelle/HOL - First Results.	ARQNL@IJCAR	2022	DBLP BibTeX RDF
16	Constantin Sander, Ike Kunze, Klaus Wehrle	Analyzing the Influence of Resource Prioritization on HTTP/3 HOL Blocking and Performance.	TMA	2022	DBLP BibTeX RDF
16	Michikazu Hirata, Yasuhiko Minamide, Tetsuya Sato 0001	Program Logic for Higher-Order Probabilistic Programs in Isabelle/HOL.	FLOPS	2022	DBLP DOI BibTeX RDF
16	Mohamed Abdelghany, Sofiène Tahar	Formalization of Functional Block Diagrams Using HOL Theorem Proving.	SBMF	2022	DBLP DOI BibTeX RDF
16	Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, Thomas Sewell	Candle: A Verified Implementation of HOL Light.	ITP	2022	DBLP DOI BibTeX RDF
16	Asta Halkjær From, Frederik Krogsdal Jacobsen	Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL.	ITP	2022	DBLP DOI BibTeX RDF
16	Mihails Milehins	An extension of the framework types-to-sets for Isabelle/HOL.	CPP	2022	DBLP DOI BibTeX RDF
16	Elif Deniz, Adnan Rashid, Osman Hasan, Sofiène Tahar	On the Formalization of the Heat Conduction Problem in HOL.	CICM	2022	DBLP DOI BibTeX RDF
16	Ciarán Dunne, J. B. Wells	Isabelle/HOL/GST: A Formal Proof Environment for Generalized Set Theories.	CICM	2022	DBLP DOI BibTeX RDF
16	Daniel Kirchner	Computer-Verified Foundations of Metaphysics and an Ontology of Natural Numbers in Isabelle/HOL.		2022	RDF
16	Zhenjiang Qian, Wei Liu, Yiyang Yao	Verification of Operating Systems for Internet of Things in Smart Cities From the Assembly Perspective Using Isabelle/HOL.	IEEE Access	2021	DBLP DOI BibTeX RDF
16	Haitao Wang 0024, Lihua Song	Study of Isabelle/HOL on Formal Algorithm Analysis and Code Generation.	IEEE Access	2021	DBLP DOI BibTeX RDF
16	Martin Raska, Stepán Starosta	Producing symmetrical facts for lists induced by the list reversal mapping in Isabelle/HOL.	CoRR	2021	DBLP BibTeX RDF
16	Laura Kovács, Hanna Lachnitt, Stefan Szeider	Formalizing Graph Trail Properties in Isabelle/HOL.	CoRR	2021	DBLP BibTeX RDF
16	Asta Halkjær From, Frederik Krogsdal Jacobsen, Jørgen Villadsen	SeCaV: A Sequent Calculus Verifier in Isabelle/HOL.	LSFA	2021	DBLP DOI BibTeX RDF
16	Mnacho Echenim, Mehdi Mhalla	Quantum projective measurements and the CHSH inequality in Isabelle/HOL.	CoRR	2021	DBLP BibTeX RDF
16	Richard Schmoetten, Jake E. Palmer, Jacques D. Fleuriot	Towards Formalising Schutz' Axioms for Minkowski Spacetime in Isabelle/HOL.	CoRR	2021	DBLP BibTeX RDF
16	Shahid Ali Murtza, Waqar Ahmed, Adnan Rashid, Osman Hasan	Towards the Formal Performance Analysis of Multistate Coherent Systems using HOL Theorem Proving.	CoRR	2021	DBLP BibTeX RDF
16	David Fuenmayor	Topological semantics for paraconsistent and paracomplete logics in Isabelle/HOL.	CoRR	2021	DBLP BibTeX RDF
16	Christoph Benzmüller, Sebastian Reiche	Modeling and Automating Public Announcement Logic with Relativized Common Knowledge as a Fragment of HOL in LogiKEy.	CoRR	2021	DBLP BibTeX RDF
16	Simon Foster 0001, Chung-Kil Hur, Jim Woodcock 0001	Formally Verified Simulations of State-Rich Processes using Interaction Trees in Isabelle/HOL.	CoRR	2021	DBLP BibTeX RDF
16	Angeliki Koutsoukou-Argyraki, Wenda Li, Lawrence C. Paulson	Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL.	CoRR	2021	DBLP BibTeX RDF
16	Simon Foster 0001, Jonathan Julián Huerta y Munive, Mario Gleirscher, Georg Struth	Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs.	CoRR	2021	DBLP BibTeX RDF
16	Mark Chevallier, Jacques D. Fleuriot	Formalising the Foundations of Discrete Reinforcement Learning in Isabelle/HOL.	CoRR	2021	DBLP BibTeX RDF
16	Thomas Hickman, Christian Pardillo Laursen, Simon Foster 0001	Certifying Differential Equation Solutions from Computer Algebra Systems in Isabelle/HOL.	CoRR	2021	DBLP BibTeX RDF
16	Lukas Stevens, Tobias Nipkow	A Verified Decision Procedure for Orders in Isabelle/HOL.	CoRR	2021	DBLP BibTeX RDF
16	Andreas Lochbihler, S. Reza Sefidgar	Constructive Cryptography in HOL: the Communication Modeling Aspect.	Arch. Formal Proofs	2021	DBLP BibTeX RDF
16	Christoph Benzmüller	Exploring Simplified Variants of Gödel's Ontological Argument in Isabelle/HOL.	Arch. Formal Proofs	2021	DBLP BibTeX RDF
16	Christoph Benzmüller, Sebastian Reiche	Automating Public Announcement Logic and the Wise Men Puzzle in Isabelle/HOL.	Arch. Formal Proofs	2021	DBLP BibTeX RDF
16	Mihails Milehins	Category Theory for ZFC in HOL I: Foundations: Design Patterns, Set Theory, Digraphs, Semicategories.	Arch. Formal Proofs	2021	DBLP BibTeX RDF
16	Mihails Milehins	Category Theory for ZFC in HOL II: Elementary Theory of 1-Categories.	Arch. Formal Proofs	2021	DBLP BibTeX RDF
16	Mihails Milehins	Category Theory for ZFC in HOL III: Universal Constructions.	Arch. Formal Proofs	2021	DBLP BibTeX RDF
16	Zhé Hóu, David Sanán, Alwen Tiu, Yang Liu 0003, Koh Chuen Hoa, Jin Song Dong	An Isabelle/HOL Formalisation of the SPARC Instruction Set Architecture and the TSO Memory Model.	J. Autom. Reason.	2021	DBLP DOI BibTeX RDF
16	Yong Guan, Jingzhi Zhang, Guohui Wang, Ximeng Li 0003, Zhiping Shi 0002, Yongdong Li	Formalization of Euler-Lagrange Equation Set Based on Variational Calculus in HOL Light.	J. Autom. Reason.	2021	DBLP DOI BibTeX RDF
16	Anthony Bordg, Hanna Lachnitt, Yijun He	Certified Quantum Computation in Isabelle/HOL.	J. Autom. Reason.	2021	DBLP DOI BibTeX RDF
16	Miriam Backens	A Full Dichotomy for $\hol^{c}$, Inspired by Quantum Computation.	SIAM J. Comput.	2021	DBLP DOI BibTeX RDF
16	Asta Halkjær From, Anders Schlichtkrull, Jørgen Villadsen	A Sequent Calculus for First-Order Logic Formalized in Isabelle/HOL.	CILC	2021	DBLP BibTeX RDF
16	Simon Foster 0001, Jonathan Julián Huerta y Munive, Mario Gleirscher, Georg Struth	Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs.	FM	2021	DBLP DOI BibTeX RDF
16	Matt Griffin, Brijesh Dongol	Verifying Secure Speculation in Isabelle/HOL.	FM	2021	DBLP DOI BibTeX RDF
16	Lukas Stevens, Tobias Nipkow	A Verified Decision Procedure for Orders in Isabelle/HOL.	ATVA	2021	DBLP DOI BibTeX RDF
16	Stepan Holub, Stepán Starosta	Lyndon Words Formalized in Isabelle/HOL.	DLT	2021	DBLP DOI BibTeX RDF
16	Alexander Birch Jensen	Towards Verifying GOAL Agents in Isabelle/HOL.	ICAART (1)	2021	DBLP DOI BibTeX RDF
16	Christoph Benzmüller, David Fuenmayor	Value-Oriented Legal Argumentation in Isabelle/HOL.	ITP	2021	DBLP DOI BibTeX RDF
16	Max W. Haslbeck, René Thiemann	An Isabelle/HOL formalization of AProVE's termination method for LLVM IR.	CPP	2021	DBLP DOI BibTeX RDF
16	Simon Foster 0001, Chung-Kil Hur, Jim Woodcock 0001	Formally Verified Simulations of State-Rich Processes Using Interaction Trees in Isabelle/HOL.	CONCUR	2021	DBLP DOI BibTeX RDF
16	Yutaka Nagashima	Faster Smarter Proof by Induction in Isabelle/HOL.	IJCAI	2021	DBLP DOI BibTeX RDF
16	Diego Marmsoler, Achim D. Brucker	A Denotational Semantics of Solidity in Isabelle/HOL.	SEFM	2021	DBLP DOI BibTeX RDF
16	Stepan Holub	Computing the Border Array in Isabelle/HOL (short paper).	CICM Workshops	2021	DBLP BibTeX RDF
16	Martin Raska, Stepán Starosta	Producing Symmetrical Facts for lIsts induced by the List Reversal Mapping in Isabelle/HOL (short paper).	CICM Workshops	2021	DBLP BibTeX RDF
16	Mohamed Abdelghany, Sofiène Tahar	Formalization of RBD-Based Cause Consequence Analysis in HOL.	CICM	2021	DBLP DOI BibTeX RDF
16	Asta Halkjær From, Agnes Moesgård Eschen, Jørgen Villadsen	Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL.	CICM	2021	DBLP DOI BibTeX RDF
16	Alfio Ricardo de Brito Martini	Reasoning about Partial Correctness Assertions in Isabelle/HOL.	RITA	2020	DBLP DOI BibTeX RDF
16	Sebastian Reiche, Christoph Benzmüller	Public Announcement Logic in HOL.	CoRR	2020	DBLP BibTeX RDF
16	Yutaka Nagashima	Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description).	CoRR	2020	DBLP BibTeX RDF
16	Sadegh Dalvandi, Brijesh Dongol, Simon Doherty	Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL.	CoRR	2020	DBLP BibTeX RDF
16	Yutaka Nagashima	Smart Induction for Isabelle/HOL (System Description).	CoRR	2020	DBLP BibTeX RDF
16	Asta Halkjær From, Jørgen Villadsen, Patrick Blackburn	Isabelle/HOL as a Meta-Language for Teaching Logic.	ThEdu@IJCAR	2020	DBLP DOI BibTeX RDF
16	Anthony Bordg, Hanna Lachnitt, Yijun He	Certified Quantum Computation in Isabelle/HOL.	CoRR	2020	DBLP BibTeX RDF
16	Yutaka Nagashima	Towards United Reasoning for Automatic Induction in Isabelle/HOL.	CoRR	2020	DBLP BibTeX RDF
16	Yutaka Nagashima	SeLFiE: Modular Semantic Reasoning for Induction in Isabelle/HOL.	CoRR	2020	DBLP BibTeX RDF
16	Johannes Åman Pohjola, Arve Gengelbach	A Mechanised Semantics for HOL with Ad-hoc Overloading.	CoRR	2020	DBLP BibTeX RDF
16	Arve Gengelbach, Johannes Åman Pohjola, Tjark Weber	Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading.	LFMTP	2020	DBLP DOI BibTeX RDF
16	Yutaka Nagashima	Faster Smarter Induction in Isabelle/HOL with SeLFiE.	CoRR	2020	DBLP BibTeX RDF
16	Petros Papapanagiotou, Jacques D. Fleuriot	Object-Level Reasoning with Logics Encoded in HOL Light.	LFMTP	2020	DBLP DOI BibTeX RDF
16	Filip Maric, Sana Stojanovic-Durdevic	Formalizing IMO Problems and Solutions in Isabelle/HOL.	ThEdu@IJCAR	2020	DBLP DOI BibTeX RDF
16	Salomon Sickert	An Efficient Normalisation Procedure for Linear Temporal Logic: Isabelle/HOL Formalisation.	Arch. Formal Proofs	2020	DBLP BibTeX RDF
16	Safouan Taha, Burkhart Wolff, Lina Ye	The HOL-CSP Refinement Toolkit.	Arch. Formal Proofs	2020	DBLP BibTeX RDF
16	René Thiemann, Ralph Bottesch, Jose Divasón, Max W. Haslbeck, Sebastiaan J. C. Joosten, Akihisa Yamada 0002	Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL.	J. Autom. Reason.	2020	DBLP DOI BibTeX RDF
16	Christoph Benzmüller, Dana S. Scott	Automating Free Logic in HOL, with an Experimental Application in Category Theory.	J. Autom. Reason.	2020	DBLP DOI BibTeX RDF
16	Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada 0002	A Verified Implementation of Algebraic Numbers in Isabelle/HOL.	J. Autom. Reason.	2020	DBLP DOI BibTeX RDF
16	Mnacho Echenim, Hervé Guiol, Nicolas Peltier	Formalizing the Cox-Ross-Rubinstein Pricing of European Derivatives in Isabelle/HOL.	J. Autom. Reason.	2020	DBLP DOI BibTeX RDF
16	Oskar Abrahamsson, Son Ho, Hrutvik Kanabar, Ramana Kumar, Magnus O. Myreen, Michael Norrish, Yong Kiam Tan	Proof-Producing Synthesis of CakeML from Monadic HOL Functions.	J. Autom. Reason.	2020	DBLP DOI BibTeX RDF
16	Wenda Li, Lawrence C. Paulson	Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOL.	J. Autom. Reason.	2020	DBLP DOI BibTeX RDF
16	Adnan Rashid, Osman Hasan	Formal Verification of Robotic Cell Injection systems up to 4-DOF using HOL Light.	Formal Aspects Comput.	2020	DBLP DOI BibTeX RDF
16	Seyed Mehdi Mohtavipour, Morteza Mollajafari, Ali Naseri	A novel packet exchanging strategy for preventing HoL-blocking in fat-trees.	Clust. Comput.	2020	DBLP DOI BibTeX RDF
16	Chun Tian 0001, Davide Sangiorgi	Unique solutions of contractions, CCS, and their HOL formalisation.	Inf. Comput.	2020	DBLP DOI BibTeX RDF
16	Simon Foster 0001, Jonathan Julián Huerta y Munive, Georg Struth	Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL.	RAMiCS	2020	DBLP DOI BibTeX RDF