|
|
Venues (Conferences, Journals, ...)
|
|
GrowBag graphs for keyword ? (Num. hits/coverage)
Group by:
The graphs summarize 788 occurrences of 554 keywords
|
|
|
Results
Found 5857 publication records. Showing 5134 according to the selection in the facets
Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
27 | Jesper Bengtson, Joachim Parrow |
Psi-calculi in Isabelle. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pp. 99-114, 2009, Springer, 978-3-642-03358-2. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
27 | Jinshuang Wang, Huabing Yang, Xingyuan Zhang |
Liveness Reasoning with Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pp. 485-499, 2009, Springer, 978-3-642-03358-2. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
Liveness Proof, Inductive Protocol Verification, Parametric Fairness, Probabilistic Model |
27 | Christian Urban |
Nominal Techniques in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 40(4), pp. 327-356, 2008. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
Nominal logic work, Lambda-calculus, Theorem provers |
27 | Laura I. Meikle, Jacques D. Fleuriot |
Prover's Palette: A User-Centric Approach to Verification with Isabelle and QEPCAD-B. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CAV ![In: Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings, pp. 309-313, 2008, Springer, 978-3-540-70543-7. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
27 | Lukas Bulwahn, Alexander Krauss 0001, Florian Haftmann, Levent Erkök, John Matthews |
Imperative Functional Programming with Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, pp. 134-149, 2008, Springer, 978-3-540-71065-3. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
27 | Daniel Wasserrab, Andreas Lochbihler |
Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, pp. 294-309, 2008, Springer, 978-3-540-71065-3. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
27 | Lawrence C. Paulson |
The Relative Consistency of the Axiom of Choice - Mechanized Using Isabelle/ZF. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CiE ![In: Logic and Theory of Algorithms, 4th Conference on Computability in Europe, CiE 2008, Athens, Greece, June 15-20, 2008, Proceedings, pp. 486-490, 2008, Springer, 978-3-540-69405-2. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
27 | Laura I. Meikle, Jacques D. Fleuriot |
Combining Isabelle and QEPCAD-B in the Prover's Palette. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AISC/MKM/Calculemus ![In: Intelligent Computer Mathematics, 9th International Conference, AISC 2008, 15th Symposium, Calculemus 2008, 7th International Conference, MKM 2008, Birmingham, UK, July 28 - August 1, 2008. Proceedings, pp. 315-330, 2008, Springer, 978-3-540-85109-7. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
27 | Hamdi Yahyaoui, Mourad Debbabi, Nadia Tawbi |
A Denotational Semantic Model for Validating JVML/CLDC Optimizations under Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
QSIC ![In: Seventh International Conference on Quality Software (QSIC 2007), 11-12 October 2007, Portland, Oregon, USA, pp. 348-355, 2007, IEEE Computer Society. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
27 | Christian Urban, Stefan Berghofer |
A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, pp. 498-512, 2006, Springer, 3-540-37187-7. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
Lambda-calculus, proof assistants, nominal logic, primitive recursion |
27 | Makarius Wenzel |
Structured Induction Proofs in Isabelle/Isar. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MKM ![In: Mathematical Knowledge Management, 5th International Conference, MKM 2006, Wokingham, UK, August 11-12, 2006, Proceedings, pp. 17-30, 2006, Springer, 3-540-37104-4. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
27 | Brian Huffman, John Matthews, Peter White |
Axiomatic Constructor Classes in Isabelle/HOLCF. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings, pp. 147-162, 2005, Springer, 3-540-28372-2. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
27 | Christian Urban, Christine Tasson |
Nominal Techniques in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings, pp. 38-53, 2005, Springer, 3-540-28005-7. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
theorem-assistants, Lambda-calculus, nominal logic, structural induction |
27 | Norbert Schirmer |
A Verification Environment for Sequential Imperative Programs in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic for Programming, Artificial Intelligence, and Reasoning, 11th International Conference, LPAR 2004, Montevideo, Uruguay, March 14-18, 2005, Proceedings, pp. 398-414, 2004, Springer, 3-540-25236-3. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
27 | Baris Sertkaya, Halit Oguztüzün |
Proof of the Basic Theorem on Concept Lattices in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISCIS ![In: Computer and Information Sciences - ISCIS 2004, 19th International Symposium, Kemer-Antalya, Turkey, October 27-29, 2004. Proceedings, pp. 976-985, 2004, Springer, 3-540-23526-4. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
27 | Jeremy Avigad, Kevin Donnelly |
Formalizing O Notation in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning - Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings, pp. 357-371, 2004, Springer, 3-540-22345-2. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
27 | Stefan Berghofer, Tobias Nipkow |
Random Testing in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SEFM ![In: 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004), 28-30 September 2004, Beijing, China, pp. 230-239, 2004, IEEE Computer Society, 0-7695-2222-X. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
27 | Wolfram Kahl |
Calculational Relation-Algebraic Proofs in Isabelle/Isar. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RelMiCS ![In: Relational and Kleene-Algebraic Methods in Computer Science: 7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra, Bad Malente, Germany, May 12-17, 2003, Revised Selected Papers, pp. 178-190, 2003, Springer, 3-540-22145-X. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
27 | Leonor Prensa Nieto |
The Rely-Guarantee Method in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ESOP ![In: Programming Languages and Systems, 12th European Symposium on Programming, ESOP 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, pp. 348-362, 2003, Springer, 3-540-00886-1. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
27 | Stefan Berghofer |
A Constructive Proof of Higman's Lemma in Isabelle. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers, pp. 66-82, 2003, Springer, 3-540-22164-6. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
27 | Clemens Ballarin |
Locales and Locale Expressions in Isabelle/Isar. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers, pp. 34-50, 2003, Springer, 3-540-22164-6. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
27 | Yasuhiko Minamide, Koji Okuma |
Verifying CPS transformations in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: Eighth ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2003, Uppsala, Sweden, August 2003, 2003, ACM, 978-1-58113-800-9. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
program transformation, theorem proving, correctness proofs |
27 | Lucas Dixon, Jacques D. Fleuriot |
IsaPlanner: A Prototype Proof Planner in Isabelle. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings, pp. 279-283, 2003, Springer, 3-540-40559-3. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
27 | Martin Strecker |
Investigating Type-Certifying Compilation with Isabelle. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic for Programming, Artificial Intelligence, and Reasoning, 9th International Conference, LPAR 2002, Tbilisi, Georgia, October 14-18, 2002, Proceedings, pp. 403-417, 2002, Springer, 3-540-00010-0. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
27 | Gertrud Bauer, Tobias Nipkow |
The 5 Colour Theorem in Isabelle/Isar. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, Proceedings, pp. 67-82, 2002, Springer, 3-540-44039-9. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
27 | Martin Strecker |
Formal Verification of a Java Compiler in Isabelle. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-18, 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002, Proceedings, pp. 63-77, 2002, Springer, 3-540-43931-5. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
27 | David Hemer, Ian J. Hayes, Paul A. Strooper |
Refinement Calculus for Logic Programming in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, UK, September 3-6, 2001, Proceedings, pp. 249-264, 2001, Springer, 3-540-42525-X. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
27 | Stephan Merz |
Weak Alternating Automata in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings, pp. 424-441, 2000, Springer, 3-540-67863-8. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
27 | Jacques D. Fleuriot |
On the Mechanization of Real Analysis in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings, pp. 145-161, 2000, Springer, 3-540-67863-8. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
27 | Florian Kammüller, Markus Wenzel 0001, Lawrence C. Paulson |
Locales - A Sectioning Concept for Isabelle. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings, pp. 149-166, 1999, Springer, 3-540-66463-7. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
27 | Jacques D. Fleuriot, Lawrence C. Paulson |
Proving Newton's Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Automated Deduction in Geometry ![In: Automated Deduction in Geometry, Second International Workshop, ADG'98, Beijing, China, August 1-3, 1998, Proceedings, pp. 47-66, 1998, Springer, 3-540-66672-9. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
27 | Jeremy E. Dawson, Rajeev Goré |
A Mechanisation of Classical Modal Tense Logics Using Isabelle. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Australian Joint Conference on Artificial Intelligence ![In: Advanced Topics in Artificial Intelligence, 11th Australian Joint Conference on Artificial Intelligence, AI '98, Brisbane, Australia, July 13-17, 1998, Selected Papers, pp. 107-118, 1998, Springer, 3-540-65138-1. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
logics for knowledge and belief, display logic, sequent calculus, automated deduction, hybrid logics, tense logic |
27 | Sten Agerholm, Jacob Frost |
An Isabelle-Based Theorem Prover for VDM-SL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings, pp. 1-16, 1997, Springer, 3-540-63379-0. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
27 | Martin Simons 0001 |
Proof Presentation for Isabelle. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings, pp. 259-274, 1997, Springer, 3-540-63379-0. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
27 | Olaf Müller, Tobias Nipkow |
Traces of I/O-Automata in Isabelle/HOLCF. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TAPSOFT ![In: TAPSOFT'97: Theory and Practice of Software Development, 7th International Joint Conference CAAP/FASE, Lille, France, April 14-18, 1997, Proceedings, pp. 580-594, 1997, Springer, 3-540-62781-2. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
27 | Seán Matthews |
Implementing FS0 in Isabelle: Adding Structure at the Metalevel. ![Search on Bibsonomy](Pics/bibsonomy.png) |
DISCO ![In: Design and Implementation of Symbolic Computation Systems, International Symposium, DISCO '96, Karlsruhe, Germany, September 18-20, 1996, Proceedings, pp. 228-239, 1996, Springer, 3-540-61697-7. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
21 | Jasmin Christian Blanchette |
Proof Pearl: Mechanizing the Textbook Proof of Huffman's Algorithm. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 43(1), pp. 1-18, 2009. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
Interactive theorem provers, Huffman coding, Higher-order logic |
21 | Javier de Dios, Ricardo Peña-Marí |
Formal Certification of a Resource-Aware Language Implementation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pp. 196-211, 2009, Springer, 978-3-642-03358-2. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
memory management, functional languages, compiler verification |
21 | Stefan Berghofer, Markus Reiter |
Formalizing the Logic-Automaton Connection. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pp. 147-163, 2009, Springer, 978-3-642-03358-2. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
21 | Jeremy E. Dawson, Alwen Tiu |
Formalising Observer Theory for Environment-Sensitive Bisimulation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pp. 180-195, 2009, Springer, 978-3-642-03358-2. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
21 | Rafal Kolanski, Gerwin Klein |
Types, Maps and Separation Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pp. 276-292, 2009, Springer, 978-3-642-03358-2. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
21 | Christoph Lüth, Dennis Walter |
Certifiable Specification and Verification of C Programs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FM ![In: FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009. Proceedings, pp. 419-434, 2009, Springer, 978-3-642-05088-6. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
21 | Levent Erkök, John Matthews |
Pragmatic equivalence and safety checking in Cryptol. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PLPV ![In: Proceedings of the 3rd ACM Workshop Programming Languages meets Program Verification, PLPV 2009, Savannah, GA, USA, January 20, 2009, pp. 73-82, 2009, ACM, 978-1-60558-330-3. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
sat/smt solving, size polymorphism, formal methods, cryptography, theorem proving, equivalence checking |
21 | Klaus Aehlig, Florian Haftmann, Tobias Nipkow |
A Compiled Implementation of Normalization by Evaluation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, pp. 39-54, 2008, Springer, 978-3-540-71065-3. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
21 | Rok Strnisa, Peter Sewell, Matthew J. Parkinson |
The java module system: core design and semantic definition. ![Search on Bibsonomy](Pics/bibsonomy.png) |
OOPSLA ![In: Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2007, October 21-25, 2007, Montreal, Quebec, Canada, pp. 499-514, 2007, ACM, 978-1-59593-786-5. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
LJAM, superpackage, java, module, JAM |
21 | Christoph Sprenger 0001, David A. Basin |
A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings, pp. 302-318, 2007, Springer, 978-3-540-74590-7. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
21 | Jeremy E. Dawson |
Formalising Generalised Substitutions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings, pp. 54-69, 2007, Springer, 978-3-540-74590-7. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
general correctness, generalised substitution |
21 | Jesper Bengtson, Joachim Parrow |
Formalising the pi-Calculus Using Nominal Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FoSSaCS ![In: Foundations of Software Science and Computational Structures, 10th International Conference, FOSSACS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007, Braga, Portugal, March 24-April 1, 2007, Proceedings, pp. 63-77, 2007, Springer, 978-3-540-71388-3. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
21 | Amine Chaieb, Makarius Wenzel |
Context Aware Calculation and Deduction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Calculemus/MKM ![In: Towards Mechanized Mathematical Assistants, 14th Symposium, Calculemus 2007, 6th International Conference, MKM 2007, Hagenberg, Austria, June 27-30, 2007, Proceedings, pp. 27-39, 2007, Springer, 978-3-540-73083-5. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
21 | Viktor Kuncak, Martin C. Rinard |
An overview of the Jahob analysis system: project goals and current status. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IPDPS ![In: 20th International Parallel and Distributed Processing Symposium (IPDPS 2006), Proceedings, 25-29 April 2006, Rhodes Island, Greece, 2006, IEEE. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
21 | Tom Ridge, James Margetson |
A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings, pp. 294-309, 2005, Springer, 3-540-28372-2. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
21 | Laura I. Meikle, Jacques D. Fleuriot |
Mechanical Theorem Proving in Computational Geometry. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Automated Deduction in Geometry ![In: Automated Deduction in Geometry, 5th International Workshop, ADG 2004, Gainesville, FL, USA, September 16-18, 2004, Revised Papers, pp. 1-18, 2004, Springer, 3-540-31332-X. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
21 | Martin Wildmoser, Tobias Nipkow |
Certifying Machine Code Safety: Shallow Versus Deep Embedding. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 17th International Conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004, Proceedings, pp. 305-320, 2004, Springer, 3-540-23017-3. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
21 | Morten P. Lindegaard, Anne E. Haxthausen |
Proof Support for RAISE by a Reuse Approach Based on Institutions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AMAST ![In: Algebraic Methodology and Software Technology, 10th International Conference, AMAST 2004, Stirling, Scotland, UK, July 12-16, 2004, Proceedings, pp. 319-333, 2004, Springer, 3-540-22381-9. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
proof support, Institutions, algebraic semantics, HOL, RSL |
21 | Michael Drouineaud, Maksym Bortin, Paolo Torrini, Karsten Sohr |
A First Step Towards Formal Verification of Security Policy Properties for RBAC. ![Search on Bibsonomy](Pics/bibsonomy.png) |
QSIC ![In: 4th International Conference on Quality Software (QSIC 2004), 8-10 September 2004, Braunschweig, Germany, pp. 60-67, 2004, IEEE Computer Society, 0-7695-2207-6. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
21 | Jeremy E. Dawson, Rajeev Goré |
Formalised Cut Admissibility for Display Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, Proceedings, pp. 131-147, 2002, Springer, 3-540-44039-9. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
21 | Marieke Huisman |
Verification of Java's AbstractCollection Class: A Case Study. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MPC ![In: Mathematics of Program Construction, 6th International Conference, MPC 2002, Dagstuhl Castle, Germany, July 8-10, 2002, Proceedings, pp. 175-194, 2002, Springer, 3-540-43857-2. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
21 | Lawrence C. Paulson |
The Reflection Theorem: A Study in Meta-theoretic Reasoning. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-18, 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002, Proceedings, pp. 377-391, 2002, Springer, 3-540-43931-5. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
21 | David von Oheimb, Volkmar Lotz |
Formal Security Analysis with Interacting State Machines. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ESORICS ![In: Computer Security - ESORICS 2002, 7th European Symposium on Research in Computer Security, Zurich, Switzerland, October 14-16, 2002, Proceedings, pp. 212-228, 2002, Springer, 3-540-44345-2. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
21 | Steffen Helke, Florian Kammüller |
Representing Hierarchical Automata in Interactive Theorem Provers. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, UK, September 3-6, 2001, Proceedings, pp. 233-248, 2001, Springer, 3-540-42525-X. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
21 | Jacques D. Fleuriot |
Nonstandard Geometric Proofs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Automated Deduction in Geometry ![In: Automated Deduction in Geometry, Third International Workshop, ADG 2000, Zurich, Switzerland, September 25-27, 2000, Revised Papers, pp. 246-267, 2000, Springer, 3-540-42598-5. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
21 | Bernhard Reus, Tatjana Hein |
Towards a Machine-Checked Java Specification Book. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings, pp. 480-497, 2000, Springer, 3-540-67863-8. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
21 | Christine Röckl, Javier Esparza |
Proof-Checking Protocols Using Bisimulations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CONCUR ![In: CONCUR '99: Concurrency Theory, 10th International Conference, Eindhoven, The Netherlands, August 24-27, 1999, Proceedings, pp. 525-540, 1999, Springer, 3-540-66425-4. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
21 | Lawrence C. Paulson |
Inductive Analysis of the Internet Protocol TLS (Position Paper). ![Search on Bibsonomy](Pics/bibsonomy.png) |
Security Protocols Workshop ![In: Security Protocols, 6th International Workshop, Cambridge, UK, April 15-17, 1998, Proceedings, pp. 1-12, 1998, Springer, 3-540-65663-4. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
21 | Katherine A. Eastaughffe, Maris A. Ozols, Anthony Cant |
Proof Tactics for a Theory of State Machines in a Graphical Environment. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-14, 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13-17, 1997, Proceedings, pp. 366-379, 1997, Springer, 3-540-63104-6. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
21 | David R. Lester, Sava Mintchev |
Towards Machine-Checked Compiler Correctness for Higher-order Pure Functional Languages. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CSL ![In: Computer Science Logic, 8th International Workshop, CSL '94, Kazimierz, Poland, September 25-30, 1994, Selected Papers, pp. 369-381, 1994, Springer, 3-540-60017-5. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
Congruence Proof, Lambda Calculus, Denotational Semantics, Theorem Prover, Compiler Correctness |
20 | Andrei Popescu 0001, Elsa L. Gunter, Christopher J. Osborn |
Strong Normalization for System F by HOAS on Top of FOAS. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LICS ![In: Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, 11-14 July 2010, Edinburgh, United Kingdom, pp. 31-40, 2010, IEEE Computer Society, 978-0-7695-4114-3. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
Higher-Order Abstract Syntax, Isabelle/HOL, System F |
20 | Ihor Kuz, Gerwin Klein, Corey Lewis, Adam Walker |
capDL: a language for describing capability-based systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ApSys ![In: Proceedings of the 1st ACM SIGCOMM Asia-Pacific Workshop on Systems, ApSys 2010, New Delhi, India, August 30, 2010, pp. 31-36, 2010, ACM, 978-1-4503-0195-4. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
SEL4, capability distribution, capabilities, security analysis, isabelle |
20 | Patrick Schaller, Benedikt Schmidt 0002, David A. Basin, Srdjan Capkun |
Modeling and Verifying Physical Properties of Security Protocols for Wireless Networks. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CSF ![In: Proceedings of the 22nd IEEE Computer Security Foundations Symposium, CSF 2009, Port Jefferson, New York, USA, July 8-10, 2009, pp. 109-123, 2009, IEEE Computer Society, 978-0-7695-3712-2. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
Wireless Network Protocols, Security Protocols, Isabelle/HOL, Formal Security Model |
20 | Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David A. Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, Simon Winwood |
seL4: formal verification of an OS kernel. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SOSP ![In: Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, SOSP 2009, Big Sky, Montana, USA, October 11-14, 2009, pp. 207-220, 2009, ACM, 978-1-60558-752-3. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
l4, sel4, microkernel, isabelle/hol |
20 | Philip Derrin, Kevin Elphinstone, Gerwin Klein, David A. Cock, Manuel M. T. Chakravarty |
Running the manual: an approach to high-assurance microkernel development. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Haskell ![In: Proceedings of the ACM SIGPLAN Workshop on Haskell, Haskell 2006, Portland, Oregon, USA, September 17, 2006, pp. 60-71, 2006, ACM, 1-59593-489-8. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
formalisation, verification, operating systems, rapid prototyping, Haskell, monads, executable specification, Isabelle/HOL |
16 | Jonathan Julián Huerta y Munive, Simon Foster 0001, Mario Gleirscher, Georg Struth, Christian Pardillo Laursen, Thomas Hickman |
Scalable Automated Verification for Cyber-Physical Systems in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2401.12061, 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP DOI BibTeX RDF |
|
16 | Julian Parsert |
Linear Programming in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2403.19639, 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP DOI BibTeX RDF |
|
16 | Terru Stübinger, Lars Hupel |
Go Code Generation for Isabelle. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2024, 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP BibTeX RDF |
|
16 | Xavier Parent, Christoph Benzmüller |
Conditional normative reasoning as a fragment of HOL (Isabelle/HOL dataset). ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2024, 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP BibTeX RDF |
|
16 | Mnacho Echenim, Mehdi Mhalla |
A Formalization of the CHSH Inequality and Tsirelson's Upper-bound in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 68(1), pp. 2, March 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP DOI BibTeX RDF |
|
16 | Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds 0001, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli |
IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TACAS (1) ![In: Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I, pp. 311-330, 2024, Springer, 978-3-031-57245-6. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP DOI BibTeX RDF |
|
16 | Sohaib Soualah, Mohamed Khalgui, Allaoua Chaoui |
Effective Parallel Formal Verification of Reconfigurable Discrete-Event Systems Formalizing with Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AINA (2) ![In: Advanced Information Networking and Applications - Proceedings of the 38th International Conference on Advanced Information Networking and Applications (AINA-2024), Kitakyushu, Japan, 17-19 April, 2024, Volume 2, pp. 199-212, 2024, Springer, 978-3-031-57852-6. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP DOI BibTeX RDF |
|
16 | Conrad Watt, Maja Trela, Peter Lammich, Florian Märkl |
WasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for WebAssembly. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proc. ACM Program. Lang. ![In: Proc. ACM Program. Lang. 7(PLDI), pp. 100-123, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Andreas V. Hess, Sebastian Alexander Mödersheim, Achim D. Brucker |
Stateful Protocol Composition in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Trans. Priv. Secur. ![In: ACM Trans. Priv. Secur. 26(3), pp. 25:1-25:36, August 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Florian Kammüller, Dimpy Satija |
Explanation of Student Attendance AI Prediction with the Isabelle Infrastructure Framework. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Inf. ![In: Inf. 14(8), pp. 453, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Jonas Bayer, Aleksey Gonus, Christoph Benzmüller, Dana S. Scott |
Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2306.09074, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Florian Kammüller |
Higher Order Model Checking in Isabelle for Human Centric Infrastructure Security. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2312.17555, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Ata Keskin |
A Formalization of Martingales in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2311.06188, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Chelsea Edmonds, Lawrence C. Paulson |
Formal Probabilistic Methods for Combinatorial Structures in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2310.00513, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Leo Freitas |
Topologically sorting VDM-SL definitions for Isabelle/HOL translation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2304.15006, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Simon Foster 0001, Burkhart Wolff |
Automated Reasoning for Physical Quantities, Units, and Measurements in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2302.07629, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Lex Bailey, Jim Woodcock 0001, Simon Foster 0001, Roberto Metere |
Checking and Automating Confidentiality Theory in Isabelle/UTP. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2310.10658, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Marco B. Caminati |
Isabelle Formalisation of Original Representation Theorems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2306.10558, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Terru Stübinger, Lars Hupel |
Extending Isabelle/HOL's Code Generator with support for the Go programming language. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2310.02704, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Stepán Starosta |
Infinite Words and Morphic Languages Formalized in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2303.11445, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Leo Freitas, Peter Gorm Larsen |
VDM recursive functions in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2303.17457, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Mnacho Echenim, Mehdi Mhalla |
A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2306.12535, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Kevin Kappelmann |
Unification Utilities for Isabelle/ML. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2023, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP BibTeX RDF |
|
16 | Simon Roßkopf, Tobias Nipkow |
A Formalization and Proof Checker for Isabelle's Metalogic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 67(1), pp. 1, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
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) |
J. Autom. Reason. ![In: J. Autom. Reason. 67(1), pp. 2, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Richard Schmoetten, Jake E. Palmer, Jacques D. Fleuriot |
Correction: Towards Formalising Schutz' Axioms for Minkowski Spacetime in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 67(1), pp. 9, March 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
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) |
J. Log. Comput. ![In: J. Log. Comput. 33(4), pp. 818-836, June 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI 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) |
Sci. Comput. Program. ![In: Sci. Comput. Program. 230, pp. 102993, August 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
16 | Pasquale Noce |
Formal Verification of Cryptographic Protocols with Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Handb. Formal Anal. Verification Cryptogr. ![In: Handbook of Formal Analysis and Verification in Cryptography, pp. 153-212, 2023, CRC Press, 978-1-003-09005-2. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
Displaying result #101 - #200 of 5134 (100 per page; Change: ) Pages: [ <<][ 1][ 2][ 3][ 4][ 5][ 6][ 7][ 8][ 9][ 10][ 11][ >>] |
|