Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CICM ![In: Intelligent Computer Mathematics - 16th International Conference, CICM 2023, Cambridge, UK, September 5-8, 2023, Proceedings, pp. 158-173, 2023, Springer, 978-3-031-42752-7. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Mirna Dzamonja, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson |
Formalizing Ordinal Partition Relations Using Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Exp. Math. ![In: Exp. Math. 31(2), pp. 383-400, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Angeliki Koutsoukou-Argyraki, Wenda Li, Lawrence C. Paulson |
Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Exp. Math. ![In: Exp. Math. 31(2), pp. 401-412, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Katherine Kosaian, Yong Kiam Tan, André Platzer |
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2209.10978, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Ciarán Dunne, J. B. Wells |
Isabelle/HOL/GST: A Formal Proof Environment for Generalized Set Theories. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2207.12039, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Brae J. Webb, Ian J. Hayes, Mark Utting |
Verifying term graph optimizations using Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2212.06956, 2022. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2207.07499, 2022. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2212.11151, 2022. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2202.04192, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP BibTeX RDF |
|
16 | Niels Mündler, Tobias Nipkow |
A Verified Implementation of B+-Trees in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2208.09066, 2022. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2208.06642, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Marco Maggesi, Cosimo Perini Brogi |
A theorem prover and countermodel constructor for provability logic in HOL Light. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2205.03659, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Emin Karayel |
Interpolation Polynomials (in HOL-Algebra). ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2022, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP BibTeX RDF |
|
16 | Jeffrey Ketland |
Boolos's Curious Inference in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2022, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP BibTeX RDF |
|
16 | Achim D. Brucker |
Nano JSON: Working with JSON formatted data in Isabelle/HOL and Isabelle/ML. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2022, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP BibTeX RDF |
|
16 | Christoph Benzmüller, David Fuenmayor, Alexander Steen, Geoff Sutcliffe |
Automation of Boolos' Curious Inference in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2022, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP BibTeX RDF |
|
16 | Katherine Cordwell, Yong Kiam Tan, André Platzer |
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2022, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP BibTeX RDF |
|
16 | Diego Marmsoler, Achim D. Brucker |
Isabelle/Solidity: A deep Embedding of Solidity in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2022, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP BibTeX RDF |
|
16 | Sadegh Dalvandi, Brijesh Dongol, Simon Doherty, Heike Wehrheim |
Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 66(1), pp. 141-171, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Richard Schmoetten, Jake E. Palmer, Jacques D. Fleuriot |
Towards Formalising Schutz' Axioms for Minkowski Spacetime in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 66(4), pp. 953-988, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Dongchen Jiang, Bo Xu |
Generation of C++ Code from Isabelle/HOL Specification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Softw. Eng. Knowl. Eng. ![In: Int. J. Softw. Eng. Knowl. Eng. 32(7), pp. 1043-1069, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Niels Mündler, Tobias Nipkow |
A Verified Implementation of B+-Trees in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICTAC ![In: Theoretical Aspects of Computing - ICTAC 2022 - 19th International Colloquium, Tbilisi, Georgia, September 27-29, 2022, Proceedings, pp. 324-341, 2022, Springer, 978-3-031-17714-9. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Sharar Ahmadi, Brijesh Dongol, Matt Griffin |
Proving Memory Access Violations in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FTSCS ![In: Proceedings of the 8th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2022, Auckland, New Zealand, 7 December 2022, pp. 45-55, 2022, ACM, 978-1-4503-9907-4. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Xavier Parent, Christoph Benzmüller |
Automated Verification of Deontic Correspondences in Isabelle/HOL - First Results. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ARQNL@IJCAR ![In: Proceedings of the 4th International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2022) affiliated with the 11th International Joint Conference on Automated Reasoning (IJCAR 2022), Haifa, Israel, August 11, 2022., pp. 92-108, 2022, CEUR-WS.org. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP BibTeX RDF |
|
16 | Constantin Sander, Ike Kunze, Klaus Wehrle |
Analyzing the Influence of Resource Prioritization on HTTP/3 HOL Blocking and Performance. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TMA ![In: 6th Network Traffic Measurement and Analysis Conference, TMA 2022, Enschede, The Netherlands, June 27-30, 2022., 2022, IFIP, 978-3-903176-47-8. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP BibTeX RDF |
|
16 | Michikazu Hirata, Yasuhiko Minamide, Tetsuya Sato 0001 |
Program Logic for Higher-Order Probabilistic Programs in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FLOPS ![In: Functional and Logic Programming - 16th International Symposium, FLOPS 2022, Kyoto, Japan, May 10-12, 2022, Proceedings, pp. 57-74, 2022, Springer, 978-3-030-99460-0. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Mohamed Abdelghany, Sofiène Tahar |
Formalization of Functional Block Diagrams Using HOL Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SBMF ![In: Formal Methods: Foundations and Applications - 25th Brazilian Symposium, SBMF 2022, Virtual Event, December 6-9, 2022, Proceedings, pp. 22-35, 2022, Springer, 978-3-031-22475-1. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, Thomas Sewell |
Candle: A Verified Implementation of HOL Light. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 3:1-3:17, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel., pp. 13:1-13:22, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-252-5. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Mihails Milehins |
An extension of the framework types-to-sets for Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022, pp. 180-196, 2022, ACM, 978-1-4503-9182-5. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CICM ![In: Intelligent Computer Mathematics - 15th International Conference, CICM 2022, Tbilisi, Georgia, September 19-23, 2022, Proceedings, pp. 21-37, 2022, Springer, 978-3-031-16680-8. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Ciarán Dunne, J. B. Wells |
Isabelle/HOL/GST: A Formal Proof Environment for Generalized Set Theories. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CICM ![In: Intelligent Computer Mathematics - 15th International Conference, CICM 2022, Tbilisi, Georgia, September 19-23, 2022, Proceedings, pp. 38-55, 2022, Springer, 978-3-031-16680-8. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
16 | Daniel Kirchner |
Computer-Verified Foundations of Metaphysics and an Ontology of Natural Numbers in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Access ![In: IEEE Access 9, pp. 2854-2863, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Haitao Wang 0024, Lihua Song |
Study of Isabelle/HOL on Formal Algorithm Analysis and Code Generation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Access ![In: IEEE Access 9, pp. 25002-25013, 2021. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2104.11622, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
16 | Laura Kovács, Hanna Lachnitt, Stefan Szeider |
Formalizing Graph Trail Properties in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2103.03607, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
16 | Asta Halkjær From, Frederik Krogsdal Jacobsen, Jørgen Villadsen |
SeCaV: A Sequent Calculus Verifier in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LSFA ![In: Proceedings 16th Logical and Semantic Frameworks with Applications, LSFA 2021, Buenos Aires, Argentina (Online), 23rd - 24th July, 2021., pp. 38-55, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Mnacho Echenim, Mehdi Mhalla |
Quantum projective measurements and the CHSH inequality in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2103.08535, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
16 | Richard Schmoetten, Jake E. Palmer, Jacques D. Fleuriot |
Towards Formalising Schutz' Axioms for Minkowski Spacetime in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2108.10868, 2021. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2112.12976, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
16 | David Fuenmayor |
Topological semantics for paraconsistent and paracomplete logics in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2104.04284, 2021. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2111.01654, 2021. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2105.05133, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
16 | Angeliki Koutsoukou-Argyraki, Wenda Li, Lawrence C. Paulson |
Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2101.05257, 2021. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2106.05987, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
16 | Mark Chevallier, Jacques D. Fleuriot |
Formalising the Foundations of Discrete Reinforcement Learning in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2112.05996, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
16 | Thomas Hickman, Christian Pardillo Laursen, Simon Foster 0001 |
Certifying Differential Equation Solutions from Computer Algebra Systems in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2102.02679, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
16 | Lukas Stevens, Tobias Nipkow |
A Verified Decision Procedure for Orders in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2104.13117, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
16 | Andreas Lochbihler, S. Reza Sefidgar |
Constructive Cryptography in HOL: the Communication Modeling Aspect. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2021, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
16 | Christoph Benzmüller |
Exploring Simplified Variants of Gödel's Ontological Argument in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2021, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
16 | Christoph Benzmüller, Sebastian Reiche |
Automating Public Announcement Logic and the Wise Men Puzzle in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2021, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
16 | Mihails Milehins |
Category Theory for ZFC in HOL I: Foundations: Design Patterns, Set Theory, Digraphs, Semicategories. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2021, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
16 | Mihails Milehins |
Category Theory for ZFC in HOL II: Elementary Theory of 1-Categories. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2021, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
16 | Mihails Milehins |
Category Theory for ZFC in HOL III: Universal Constructions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2021, 2021. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 65(4), pp. 569-598, 2021. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 65(1), pp. 1-29, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Anthony Bordg, Hanna Lachnitt, Yijun He |
Certified Quantum Computation in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 65(5), pp. 691-709, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Miriam Backens |
A Full Dichotomy for $\hol^{c}$, Inspired by Quantum Computation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SIAM J. Comput. ![In: SIAM J. Comput. 50(6), pp. 1739-1799, 2021. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CILC ![In: Proceedings of the 36th Italian Conference on Computational Logic, Parma, Italy, September 7-9, 2021., pp. 107-121, 2021, CEUR-WS.org. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FM ![In: Formal Methods - 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings, pp. 367-386, 2021, Springer, 978-3-030-90869-0. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Matt Griffin, Brijesh Dongol |
Verifying Secure Speculation in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FM ![In: Formal Methods - 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings, pp. 43-60, 2021, Springer, 978-3-030-90869-0. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Lukas Stevens, Tobias Nipkow |
A Verified Decision Procedure for Orders in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ATVA ![In: Automated Technology for Verification and Analysis - 19th International Symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18-22, 2021, Proceedings, pp. 127-143, 2021, Springer, 978-3-030-88884-8. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Stepan Holub, Stepán Starosta |
Lyndon Words Formalized in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
DLT ![In: Developments in Language Theory - 25th International Conference, DLT 2021, Porto, Portugal, August 16-20, 2021, Proceedings, pp. 217-228, 2021, Springer, 978-3-030-81507-3. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Alexander Birch Jensen |
Towards Verifying GOAL Agents in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICAART (1) ![In: Proceedings of the 13th International Conference on Agents and Artificial Intelligence, ICAART 2021, Volume 1, Online Streaming, February 4-6, 2021., pp. 345-352, 2021, SCITEPRESS, 978-989-758-484-8. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Christoph Benzmüller, David Fuenmayor |
Value-Oriented Legal Argumentation in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)., pp. 7:1-7:20, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-188-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Max W. Haslbeck, René Thiemann |
An Isabelle/HOL formalization of AProVE's termination method for LLVM IR. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021, pp. 238-249, 2021, ACM, 978-1-4503-8299-1. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CONCUR ![In: 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference., pp. 20:1-20:18, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-203-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Yutaka Nagashima |
Faster Smarter Proof by Induction in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAI ![In: Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event / Montreal, Canada, 19-27 August 2021., pp. 1981-1988, 2021, ijcai.org. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Diego Marmsoler, Achim D. Brucker |
A Denotational Semantics of Solidity in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SEFM ![In: Software Engineering and Formal Methods - 19th International Conference, SEFM 2021, Virtual Event, December 6-10, 2021, Proceedings, pp. 403-422, 2021, Springer, 978-3-030-92123-1. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Stepan Holub |
Computing the Border Array in Isabelle/HOL (short paper). ![Search on Bibsonomy](Pics/bibsonomy.png) |
CICM Workshops ![In: Joint Proceedings of the FMM, FVPS, MathUI,NatFoM, and OpenMath Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2021 co-located with the 14th Conference on Intelligent Computer Mathematics (CICM 2021), Virtual Event, Timisoara, Romania, July 26 - 31, 2021., 2021, CEUR-WS.org. The full citation details ...](Pics/full.jpeg) |
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). ![Search on Bibsonomy](Pics/bibsonomy.png) |
CICM Workshops ![In: Joint Proceedings of the FMM, FVPS, MathUI,NatFoM, and OpenMath Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2021 co-located with the 14th Conference on Intelligent Computer Mathematics (CICM 2021), Virtual Event, Timisoara, Romania, July 26 - 31, 2021., 2021, CEUR-WS.org. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
16 | Mohamed Abdelghany, Sofiène Tahar |
Formalization of RBD-Based Cause Consequence Analysis in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CICM ![In: Intelligent Computer Mathematics - 14th International Conference, CICM 2021, Timisoara, Romania, July 26-31, 2021, Proceedings, pp. 47-64, 2021, Springer, 978-3-030-81096-2. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CICM ![In: Intelligent Computer Mathematics - 14th International Conference, CICM 2021, Timisoara, Romania, July 26-31, 2021, Proceedings, pp. 32-46, 2021, Springer, 978-3-030-81096-2. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Alfio Ricardo de Brito Martini |
Reasoning about Partial Correctness Assertions in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RITA ![In: RITA 27(3), pp. 84-101, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Sebastian Reiche, Christoph Benzmüller |
Public Announcement Logic in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2010.00810, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP BibTeX RDF |
|
16 | Yutaka Nagashima |
Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description). ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2004.10667, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP BibTeX RDF |
|
16 | Sadegh Dalvandi, Brijesh Dongol, Simon Doherty |
Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2004.02983, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP BibTeX RDF |
|
16 | Yutaka Nagashima |
Smart Induction for Isabelle/HOL (System Description). ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2001.10834, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP BibTeX RDF |
|
16 | Asta Halkjær From, Jørgen Villadsen, Patrick Blackburn |
Isabelle/HOL as a Meta-Language for Teaching Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ThEdu@IJCAR ![In: Proceedings 9th International Workshop on Theorem Proving Components for Educational Software, ThEdu@IJCAR 2020, Paris, France, 29th June 2020., pp. 18-34, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Anthony Bordg, Hanna Lachnitt, Yijun He |
Certified Quantum Computation in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2012.13925, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP BibTeX RDF |
|
16 | Yutaka Nagashima |
Towards United Reasoning for Automatic Induction in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2005.12737, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP BibTeX RDF |
|
16 | Yutaka Nagashima |
SeLFiE: Modular Semantic Reasoning for Induction in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2010.10296, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP BibTeX RDF |
|
16 | Johannes Åman Pohjola, Arve Gengelbach |
A Mechanised Semantics for HOL with Ad-hoc Overloading. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2002.10212, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP BibTeX RDF |
|
16 | Arve Gengelbach, Johannes Åman Pohjola, Tjark Weber |
Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2020, Paris, France, 29th June 2020., pp. 1-17, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Yutaka Nagashima |
Faster Smarter Induction in Isabelle/HOL with SeLFiE. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2009.09215, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP BibTeX RDF |
|
16 | Petros Papapanagiotou, Jacques D. Fleuriot |
Object-Level Reasoning with Logics Encoded in HOL Light. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2020, Paris, France, 29th June 2020., pp. 18-34, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Filip Maric, Sana Stojanovic-Durdevic |
Formalizing IMO Problems and Solutions in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ThEdu@IJCAR ![In: Proceedings 9th International Workshop on Theorem Proving Components for Educational Software, ThEdu@IJCAR 2020, Paris, France, 29th June 2020., pp. 35-55, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Salomon Sickert |
An Efficient Normalisation Procedure for Linear Temporal Logic: Isabelle/HOL Formalisation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2020, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP BibTeX RDF |
|
16 | Safouan Taha, Burkhart Wolff, Lina Ye |
The HOL-CSP Refinement Toolkit. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2020, 2020. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 64(5), pp. 827-856, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Christoph Benzmüller, Dana S. Scott |
Automating Free Logic in HOL, with an Experimental Application in Category Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 64(1), pp. 53-72, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada 0002 |
A Verified Implementation of Algebraic Numbers in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 64(3), pp. 363-389, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Mnacho Echenim, Hervé Guiol, Nicolas Peltier |
Formalizing the Cox-Ross-Rubinstein Pricing of European Derivatives in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 64(4), pp. 737-765, 2020. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 64(7), pp. 1287-1306, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Wenda Li, Lawrence C. Paulson |
Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 64(2), pp. 331-360, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Adnan Rashid, Osman Hasan |
Formal Verification of Robotic Cell Injection systems up to 4-DOF using HOL Light. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 32(2-3), pp. 229-250, 2020. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Clust. Comput. ![In: Clust. Comput. 23(2), pp. 461-482, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Chun Tian 0001, Davide Sangiorgi |
Unique solutions of contractions, CCS, and their HOL formalisation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Inf. Comput. ![In: Inf. Comput. 275, pp. 104606, 2020. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RAMiCS ![In: Relational and Algebraic Methods in Computer Science - 18th International Conference, RAMiCS 2020, Palaiseau, France, April 8-11, 2020, Proceedings [postponed]., pp. 169-186, 2020, Springer, 978-3-030-43519-6. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|