default search action

combined dblp search
author search
venue search
publication search

ask others

Jasmin Blanchette

Jasmin Christian Blanchette

> Home > Persons

Person information

affiliation: Ludwig Maximilian University of Munich, Germany
affiliation: Max Planck Institute for Informatics, Saarbrücken, Germany
affiliation: University of Lorraine, Nancy, France
affiliation (former): Vrije Universiteit Amsterdam, The Netherlands
affiliation (former): Technical University of Munich, Germany

Refine list

refinements active!

zoomed in on ?? of ?? records

view refined list in

export refined list as

showing all ?? records

2020 – today

see FAQ

What is the meaning of the colors in the publication lists?

2024
[c64]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/itp/DesharnaisTWBT24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/DesharnaisTWBT24
Martin Desharnais, Balázs Tóth, Uwe Waldmann, Jasmin Blanchette, Sophie Tourret:
A Modular Formalization of Superposition in Isabelle/HOL. ITP 2024: 12:1-12:20
2023
[j43]
- view
  - electronic edition @ isa-afp.org (open access)
  - no references & citations available
- export record
  dblp key:
  - journals/afp/BlanchetteQT23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/afp/BlanchetteQT23
Jasmin Christian Blanchette, Qi Qiu, Sophie Tourret:
Given Clause Loops. Arch. Formal Proofs 2023 (2023)
[j42]
- view
  authority control:
- export record
  dblp key:
  - journals/cacm/BentkampBNTVW23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/cacm/BentkampBNTVW23
Alexander Bentkamp, Jasmin Blanchette, Visa Nummelin, Sophie Tourret, Petar Vukmirovic, Uwe Waldmann:
Mechanical Mathematicians. Commun. ACM 66(4): 80-90 (2023)
[j41]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/BentkampBTV23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/BentkampBTV23
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic:
Superposition for Higher-Order Logic. J. Autom. Reason. 67(1): 10 (2023)
[j40]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/jar/EbnerBT23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/EbnerBT23
Gabriel Ebner, Jasmin Blanchette, Sophie Tourret:
Unifying Splitting. J. Autom. Reason. 67(2): 16 (2023)
[j39]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/lmcs/BlanchetteV23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/lmcs/BlanchetteV23
Jasmin Blanchette, Petar Vukmirovic:
SAT-Inspired Higher-Order Eliminations. Log. Methods Comput. Sci. 19(2) (2023)
[j38]
- view
  authority control:
- export record
  dblp key:
  - journals/siglog/BentkampBNTW23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/siglog/BentkampBNTW23
Alexander Bentkamp, Jasmin Blanchette, Visa Nummelin, Sophie Tourret, Uwe Waldmann:
Complete and Efficient Higher-Order Reasoning via Lambda-Superposition. ACM SIGLOG News 10(4): 25-40 (2023)
[j37]
- view
  authority control:
- export record
  dblp key:
  - journals/tocl/VukmirovicBH23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/tocl/VukmirovicBH23
Petar Vukmirovic, Jasmin Blanchette, Marijn J. H. Heule:
SAT-Inspired Eliminations for Superposition. ACM Trans. Comput. Log. 24(1): 7:1-7:25 (2023)
[c63]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/cade/BlanchetteQT23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/BlanchetteQT23
Jasmin Blanchette, Qi Qiu, Sophie Tourret:
Verified Given Clause Procedures. CADE 2023: 61-77
[c62]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/frocos/NummelinBD23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/frocos/NummelinBD23
Visa Nummelin, Jasmin Blanchette, Sander R. Dahmen:
Recurrence-Driven Summations in Automated Deduction. FroCoS 2023: 23-40
[c61]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/itp/DvorakB23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/DvorakB23
Martin Dvorak, Jasmin Blanchette:
Closure Properties of General Grammars - Formally Verified. ITP 2023: 15:1-15:16
[c60]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/tacas/VukmirovicBS23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/VukmirovicBS23
Petar Vukmirovic, Jasmin Blanchette, Stephan Schulz:
Extending a High-Performance Prover to Higher-Order Logic. TACAS (2) 2023: 111-129
[e7]
- view
- export record
  dblp key:
  - conf/mkm/2021w
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/mkm/2021w
Jasmin Blanchette, James H. Davenport, Peter Koepke, Michael Kohlhase, Andrea Kohlhase, Adam Naumowicz, Dennis Müller, Yasmine Sharoda, Claudio Sacerdoti Coen:
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. CEUR Workshop Proceedings 3377, CEUR-WS.org 2023 [contents]
[i7]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2302-06420
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2302-06420
Martin Dvorak, Jasmin Blanchette:
Closure Properties of Unrestricted Grammars - Formally Verified. CoRR abs/2302.06420 (2023)
2022
[j36]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/WaldmannTRB22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/WaldmannTRB22
Uwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Blanchette:
A Comprehensive Framework for Saturation Theorem Proving. J. Autom. Reason. 66(4): 499-539 (2022)
[j35]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/VukmirovicBBCNT22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/VukmirovicBBCNT22
Petar Vukmirovic, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, Sophie Tourret:
Making Higher-Order Superposition Work. J. Autom. Reason. 66(4): 541-564 (2022)
[j34]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/sttt/VukmirovicBCS22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/sttt/VukmirovicBCS22
Petar Vukmirovic, Jasmin Blanchette, Simon Cruanes, Stephan Schulz:
Extending a brainiac prover to lambda-free higher-order logic. Int. J. Softw. Tools Technol. Transf. 24(1): 67-87 (2022)
[c59]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/itp/DesharnaisVBW22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/DesharnaisVBW22
Martin Desharnais, Petar Vukmirovic, Jasmin Blanchette, Makarius Wenzel:
Seventeen Provers Under the Hammer. ITP 2022: 8:1-8:18
[e6]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/2022
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/2022
Jasmin Blanchette, Laura Kovács, Dirk Pattinson:
Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings. Lecture Notes in Computer Science 13385, Springer 2022, ISBN 978-3-031-10768-9 [contents]
[i6]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2208-07775
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2208-07775
Jasmin Blanchette, Petar Vukmirovic:
SAT-Inspired Higher-Order Eliminations. CoRR abs/2208.07775 (2022)
2021
[j33]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/Blanchette21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/Blanchette21
Jasmin Blanchette:
Message from the New Editor-in-Chief. J. Autom. Reason. 65(2): 155 (2021)
[j32]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/jar/BentkampBTVW21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/BentkampBTVW21
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic, Uwe Waldmann:
Superposition with Lambdas. J. Autom. Reason. 65(7): 893-940 (2021)
[j31]
- view
  - electronic edition @ episciences.org (open access)
  - no references & citations available
- export record
  dblp key:
  - journals/lmcs/BentkampBCW21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/lmcs/BentkampBCW21
Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Uwe Waldmann:
Superposition for Lambda-Free Higher-Order Logic. Log. Methods Comput. Sci. 17(2) (2021)
[c58]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/cade/EbnerBT21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/EbnerBT21
Gabriel Ebner, Jasmin Blanchette, Sophie Tourret:
A Unifying Splitting Framework. CADE 2021: 344-360
[c57]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/cade/BentkampBTV21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/BentkampBTV21
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic:
Superposition for Full Higher-order Logic. CADE 2021: 396-412
[c56]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/cade/VukmirovicBBCNT21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/VukmirovicBBCNT21
Petar Vukmirovic, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, Sophie Tourret:
Making Higher-Order Superposition Work. CADE 2021: 415-432
[c55]
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/TourretB21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/TourretB21
Sophie Tourret, Jasmin Blanchette:
A modular Isabelle framework for verifying saturation provers. CPP 2021: 224-237
[c54]
- view
  authority control:
- export record
  dblp key:
  - conf/fmcad/VukmirovicBH21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/VukmirovicBH21
Petar Vukmirovic, Jasmin Blanchette, Marijn J. H. Heule:
SAT-Inspired Eliminations for Superposition. FMCAD 2021: 231-240
[c53]
- view
  - electronic edition @ ceur-ws.org (open access)
  - no references & citations available
- export record
  dblp key:
  - conf/mkm/BlanchetteN21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/mkm/BlanchetteN21
Jasmin Blanchette, Adam Naumowicz:
FMM Preface. CICM Workshops 2021
[d2]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - data/10/VukmirovicBH21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/10/VukmirovicBH21
Petar Vukmirovic, Jasmin Blanchette, Marijn J. H. Heule:
SAT-Inspired Eliminations for Superposition. Zenodo, 2021
[d1]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - data/10/VukmirovicBH21a
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/10/VukmirovicBH21a
Petar Vukmirovic, Jasmin Blanchette, Marijn J. H. Heule:
SAT-Inspired Eliminations for Superposition. Zenodo, 2021
[i5]
- view
  - electronic edition @ arxiv.org (open access)
  - references & citations
- export record
  dblp key:
  - journals/corr/abs-2102-00453
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2102-00453
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic, Uwe Waldmann:
Superposition with Lambdas. CoRR abs/2102.00453 (2021)
2020
[j30]
- view
  - electronic edition @ isa-afp.org (open access)
  - no references & citations available
- export record
  dblp key:
  - journals/afp/BlanchetteT20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/afp/BlanchetteT20
Jasmin Blanchette, Sophie Tourret:
Extensions to the Comprehensive Framework for Saturation Theorem Proving. Arch. Formal Proofs 2020 (2020)
[j29]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/BarbosaBFF20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/BarbosaBFF20
Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, Pascal Fontaine:
Scalable Fine-Grained Proofs for Formula Processing. J. Autom. Reason. 64(3): 485-510 (2020)
[j28]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/SchlichtkrullBT20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/SchlichtkrullBT20
Anders Schlichtkrull, Jasmin Blanchette, Dmitriy Traytel, Uwe Waldmann:
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. J. Autom. Reason. 64(7): 1169-1195 (2020)
[c52]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/WaldmannTRB20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/WaldmannTRB20
Uwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Blanchette:
A Comprehensive Framework for Saturation Theorem Proving. IJCAR (1) 2020: 316-334
[e5]
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/2020
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/2020
Jasmin Blanchette, Catalin Hritcu:
Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020. ACM 2020, ISBN 978-1-4503-7097-4 [contents]
[i4]
- view
  - electronic edition @ arxiv.org (open access)
  - references & citations
- export record
  dblp key:
  - journals/corr/abs-2005-02094
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2005-02094
Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Uwe Waldmann:
Superposition for Lambda-Free Higher-Order Logic. CoRR abs/2005.02094 (2020)

2010 – 2019

see FAQ

What is the meaning of the colors in the publication lists?

2019
[j27]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/jar/BlanchetteM19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/BlanchetteM19
Jasmin Christian Blanchette, Stephan Merz:
Selected Extended Papers of ITP 2016: Preface. J. Autom. Reason. 62(2): 169-170 (2019)
[j26]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/jar/BentkampBK19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/BentkampBK19
Alexander Bentkamp, Jasmin Christian Blanchette, Dietrich Klakow:
A Formal Proof of the Expressiveness of Deep Learning. J. Autom. Reason. 63(2): 347-368 (2019)
[j25]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/pacmpl/BlanchetteGPT19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/pacmpl/BlanchetteGPT19
Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, Dmitriy Traytel:
Bindings as bounded natural functors. Proc. ACM Program. Lang. 3(POPL): 22:1-22:34 (2019)
[j24]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/sosym/BlanchetteBPKTW19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/sosym/BlanchetteBPKTW19
Jasmin Blanchette, Francis Bordeleau, Alfonso Pierantonio, Nikolai Kosmatov, Gabriele Taentzer, Manuel Wimmer:
Introduction to the STAF 2015 special section. Softw. Syst. Model. 18(1): 191-193 (2019)
[c51]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/BentkampBTVW19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/BentkampBTVW19
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic, Uwe Waldmann:
Superposition with Lambdas. CADE 2019: 55-73
[c50]
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Blanchette19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Blanchette19
Jasmin Christian Blanchette:
Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk). CPP 2019: 1-13
[c49]
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/SchlichtkrullBT19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/SchlichtkrullBT19
Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel:
A verified prover based on ordered resolution. CPP 2019: 152-165
[c48]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/tacas/VukmirovicBCS19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/VukmirovicBCS19
Petar Vukmirovic, Jasmin Christian Blanchette, Simon Cruanes, Stephan Schulz:
Extending a Brainiac Prover to Lambda-Free Higher-Order Logic. TACAS (1) 2019: 192-210
2018
[j23]
- view
  - electronic edition @ isa-afp.org (open access)
  - no references & citations available
- export record
  dblp key:
  - journals/afp/SchlichtkrullBT18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/afp/SchlichtkrullBT18
Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, Uwe Waldmann:
Formalization of Bachmair and Ganzinger's Ordered Resolution Prover. Arch. Formal Proofs 2018 (2018)
[j22]
- view
  - electronic edition @ isa-afp.org (open access)
  - no references & citations available
- export record
  dblp key:
  - journals/afp/SchlichtkrullBT18a
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/afp/SchlichtkrullBT18a
Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel:
A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover. Arch. Formal Proofs 2018 (2018)
[j21]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/jar/AvigadBKPPS18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/AvigadBKPPS18
Jeremy Avigad, Jasmin Christian Blanchette, Gerwin Klein, Lawrence C. Paulson, Andrei Popescu, Gregor Snelting:
Introduction to Milestones in Interactive Theorem Proving. J. Autom. Reason. 61(1-4): 1-8 (2018)
[j20]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/jar/BlanchetteFLW18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/BlanchetteFLW18
Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich, Christoph Weidenbach:
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. J. Autom. Reason. 61(1-4): 333-365 (2018)
[c47]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/BentkampBCW18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/BentkampBCW18
Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes, Uwe Waldmann:
Superposition for Lambda-Free Higher-Order Logic. IJCAR 2018: 28-46
[c46]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/SchlichtkrullBT18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/SchlichtkrullBT18
Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, Uwe Waldmann:
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. IJCAR 2018: 89-107
[c45]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/BlanchettePR18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/BlanchettePR18
Jasmin Christian Blanchette, Nicolas Peltier, Simon Robillard:
Superposition with Datatypes and Codatatypes. IJCAR 2018: 370-387
[c44]
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/FleuryBL18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/FleuryBL18
Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich:
A verified SAT solver with watched literals using imperative HOL. CPP 2018: 158-171
2017
[j19]
- view
  - electronic edition @ isa-afp.org (open access)
  - no references & citations available
- export record
  dblp key:
  - journals/afp/BlanchettePT17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/afp/BlanchettePT17
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Abstract Soundness. Arch. Formal Proofs 2017 (2017)
[j18]
- view
  - electronic edition @ isa-afp.org (open access)
  - no references & citations available
- export record
  dblp key:
  - journals/afp/BlanchettePT17a
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/afp/BlanchettePT17a
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Operations on Bounded Natural Functors. Arch. Formal Proofs 2017 (2017)
[j17]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/BlanchettePT17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/BlanchettePT17
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Soundness and Completeness Proofs by Coinductive Methods. J. Autom. Reason. 58(1): 149-179 (2017)
[j16]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/ReynoldsB17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/ReynoldsB17
Andrew Reynolds, Jasmin Christian Blanchette:
A Decision Procedure for (Co)datatypes in SMT Solvers. J. Autom. Reason. 58(3): 341-362 (2017)
[c43]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/cade/BlanchetteF0W17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/BlanchetteF0W17
Jasmin Christian Blanchette, Pascal Fontaine, Stephan Schulz, Uwe Waldmann:
Towards Strong Higher-Order Automation for Fast Interactive Verification. ARCADE@CADE 2017: 16-23
[c42]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/BarbosaBF17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/BarbosaBF17
Haniel Barbosa, Jasmin Christian Blanchette, Pascal Fontaine:
Scalable Fine-Grained Proofs for Formula Processing. CADE 2017: 398-412
[c41]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/BeckerBWW17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/BeckerBWW17
Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand:
A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms. CADE 2017: 432-453
[c40]
- view
  authority control:
- export record
  dblp key:
  - conf/esop/BlanchetteBL0T17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/esop/BlanchetteBL0T17
Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel:
Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants. ESOP 2017: 111-140
[c39]
- view
  authority control:
- export record
  dblp key:
  - conf/fossacs/BlanchetteWW17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fossacs/BlanchetteWW17
Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand:
A Lambda-Free Higher-Order Recursive Path Order. FoSSaCS 2017: 461-479
[c38]
- view
  authority control:
- export record
  dblp key:
  - conf/frocos/BiendarraBBDFHK17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/frocos/BiendarraBBDFHK17
Julian Biendarra, Jasmin Christian Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondrej Kuncar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, Dmitriy Traytel:
Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. FroCoS 2017: 3-21
[c37]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/ijcai/BlanchetteFW17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/ijcai/BlanchetteFW17
Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach:
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. IJCAI 2017: 4786-4790
[c36]
- view
  authority control:
- export record
  dblp key:
  - conf/itp/BentkampBK17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/BentkampBK17
Alexander Bentkamp, Jasmin Christian Blanchette, Dietrich Klakow:
A Formal Proof of the Expressiveness of Deep Learning. ITP 2017: 46-64
[c35]
- view
  authority control:
- export record
  dblp key:
  - conf/lics/BlanchetteM0T17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lics/BlanchetteM0T17
Jasmin Christian Blanchette, Fabian Meier, Andrei Popescu, Dmitriy Traytel:
Foundational nonuniform (Co)datatypes for higher-order logic. LICS 2017: 1-12
[c34]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/rta/BlanchetteFT17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/rta/BlanchetteFT17
Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel:
Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL. FSCD 2017: 11:1-11:18
[c33]
- view
  authority control:
- export record
  dblp key:
  - journals/corr/abs-1712-01486
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1712-01486
Haniel Barbosa, Jasmin Christian Blanchette, Simon Cruanes, Daniel El Ouraoui, Pascal Fontaine:
Language and Proofs for Higher-Order SMT (Work in Progress). PxTP 2017: 15-22
[i3]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/dagstuhl-reports/BlanchetteFST17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/dagstuhl-reports/BlanchetteFST17
Jasmin Christian Blanchette, Carsten Fuhs, Viorica Sofronie-Stokkermans, Cesare Tinelli:
Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371). Dagstuhl Reports 7(9): 26-46 (2017)
2016
[j15]
- view
  - electronic edition @ isa-afp.org (open access)
  - no references & citations available
- export record
  dblp key:
  - journals/afp/BeckerBWW16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/afp/BeckerBWW16
Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand:
Formalization of Knuth-Bendix Orders for Lambda-Free Higher-Order Terms. Arch. Formal Proofs 2016 (2016)
[j14]
- view
  - electronic edition @ isa-afp.org (open access)
  - no references & citations available
- export record
  dblp key:
  - journals/afp/BlanchetteFT16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/afp/BlanchetteFT16
Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel:
Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals. Arch. Formal Proofs 2016 (2016)
[j13]
- view
  - electronic edition @ isa-afp.org (open access)
  - no references & citations available
- export record
  dblp key:
  - journals/afp/BlanchetteWW16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/afp/BlanchetteWW16
Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand:
Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms. Arch. Formal Proofs 2016 (2016)
[j12]
- view
  authority control:
- export record
  dblp key:
  - journals/corr/BlanchetteB0S16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/BlanchetteB0S16
Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, Nicholas Smallbone:
Encoding Monomorphic and Polymorphic Types. Log. Methods Comput. Sci. 12(4) (2016)
[j11]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/BlanchetteBFSS16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/BlanchetteBFSS16
Jasmin Christian Blanchette, Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka, Albert Steckermeier:
Semi-intelligible Isar Proofs from Machine-Generated Proofs. J. Autom. Reason. 56(2): 155-200 (2016)
[j10]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/BlanchetteGKKU16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/BlanchetteGKKU16
Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, Josef Urban:
A Learning-Based Fact Selector for Isabelle/HOL. J. Autom. Reason. 57(3): 219-244 (2016)
[j9]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/jfrea/BlanchetteKPU16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jfrea/BlanchetteKPU16
Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, Josef Urban:
Hammering towards QED. J. Formaliz. Reason. 9(1): 101-148 (2016)
[c32]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/BlanchetteFW16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/BlanchetteFW16
Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach:
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. IJCAR 2016: 25-44
[c31]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/ReynoldsBCT16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/ReynoldsBCT16
Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, Cesare Tinelli:
Model Finding for Recursive Functions in SMT. IJCAR 2016: 133-151
[c30]
- view
  - electronic edition @ ijcai.org (open access)
  - no references & citations available
- export record
  dblp key:
  - conf/ijcai/ReynoldsB16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/ijcai/ReynoldsB16
Andrew Reynolds, Jasmin Christian Blanchette:
A Decision Procedure for (Co)datatypes in SMT Solvers. IJCAI 2016: 4205-4209
[c29]
- view
  authority control:
- export record
  dblp key:
  - journals/corr/CruanesB16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/CruanesB16
Simon Cruanes, Jasmin Christian Blanchette:
Extending Nunchaku to Dependent Type Theory. HaTT@IJCAR 2016: 3-12
[e4]
- view
  authority control:
- export record
  dblp key:
  - conf/itp/2016
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/2016
Jasmin Christian Blanchette, Stephan Merz:
Interactive Theorem Proving - 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings. Lecture Notes in Computer Science 9807, Springer 2016, ISBN 978-3-319-43143-7 [contents]
[e3]
- view
  authority control:
- export record
  dblp key:
  - journals/corr/BlanchetteK16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/BlanchetteK16
Jasmin Christian Blanchette, Cezary Kaliszyk:
Proceedings First International Workshop on Hammers for Type Theories, HaTT@IJCAR 2016, Coimbra, Portugal, July 1, 2016. EPTCS 210, 2016 [contents]
2015
[c28]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/ReynoldsB15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/ReynoldsB15
Andrew Reynolds, Jasmin Christian Blanchette:
A Decision Procedure for (Co)datatypes in SMT Solvers. CADE 2015: 197-213
[c27]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/esop/Blanchette0T15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/esop/Blanchette0T15
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Witnessing (Co)datatypes. ESOP 2015: 359-382
[c26]
- view
  authority control:
- export record
  dblp key:
  - conf/icfp/Blanchette0T15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/icfp/Blanchette0T15
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Foundational extensible corecursion: a proof assistant perspective. ICFP 2015: 192-204
[c25]
- view
  authority control:
- export record
  dblp key:
  - conf/mkm/BlanchetteHMN15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/mkm/BlanchetteHMN15
Jasmin Christian Blanchette, Max W. Haslbeck, Daniel Matichuk, Tobias Nipkow:
Mining the Archive of Formal Proofs. CICM 2015: 3-17
[e2]
- view
  authority control:
- export record
  dblp key:
  - conf/tap/2015
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tap/2015
Jasmin Christian Blanchette, Nikolai Kosmatov:
Tests and Proofs - 9th International Conference, TAP@STAF 2015, L'Aquila, Italy, July 22-24, 2015. Proceedings. Lecture Notes in Computer Science 9154, Springer 2015, ISBN 978-3-319-21214-2 [contents]
[i2]
- view
  - electronic edition @ arxiv.org (open access)
  - references & citations
- export record
  dblp key:
  - journals/corr/Blanchette0T15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/Blanchette0T15
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Foundational Extensible Corecursion. CoRR abs/1501.05425 (2015)
[i1]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/dagstuhl-reports/BjornerBSW15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/dagstuhl-reports/BjornerBSW15
Nikolaj S. Bjørner, Jasmin Christian Blanchette, Viorica Sofronie-Stokkermans, Christoph Weidenbach:
Information from Deduction: Models and Proofs (Dagstuhl Seminar 15381). Dagstuhl Reports 5(9): 18-37 (2015)
2014
[j8]
- view
  - electronic edition @ isa-afp.org (open access)
  - no references & citations available
- export record
  dblp key:
  - journals/afp/Blanchette0T14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/afp/Blanchette0T14
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Abstract Completeness. Arch. Formal Proofs 2014 (2014)
[c24]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/cade/Blanchette14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/Blanchette14
Jasmin Christian Blanchette:
My Life with an Automatic Theorem Prover. Vampire Workshop 2014: 1-7
[c23]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/Blanchette0T14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/Blanchette0T14
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Unified Classical Logic Completeness - A Coinductive Pearl. IJCAR 2014: 46-60
[c22]
- view
  authority control:
- export record
  dblp key:
  - conf/haskell/BlanchetteHNNT14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/haskell/BlanchetteHNNT14
Jasmin Christian Blanchette, Lars Hupel, Tobias Nipkow, Lars Noschinski, Dmitriy Traytel:
Experience report: the next 1100 Haskell programmers. Haskell 2014: 25-30
[c21]
- view
  authority control:
- export record
  dblp key:
  - conf/itp/BlanchetteHLP0T14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/BlanchetteHLP0T14
Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, Dmitriy Traytel:
Truly Modular (Co)datatypes for Isabelle/HOL. ITP 2014: 93-110
[c20]
- view
  authority control:
- export record
  dblp key:
  - conf/itp/Blanchette0T14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/Blanchette0T14
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Cardinals in Isabelle/HOL. ITP 2014: 111-127
2013
[j7]
- view
  - electronic edition @ isa-afp.org (open access)
  - no references & citations available
- export record
  dblp key:
  - journals/afp/Blanchette013
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/afp/Blanchette013
Jasmin Christian Blanchette, Andrei Popescu:
Sound and Complete Sort Encodings for First-Order Logic. Arch. Formal Proofs 2013 (2013)
[j6]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/japll/SultanaBP13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/japll/SultanaBP13
Nik Sultana, Jasmin Christian Blanchette, Lawrence C. Paulson:
LEO-II and Satallax on the Sledgehammer test bench. J. Appl. Log. 11(1): 91-102 (2013)
[j5]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/BlanchetteBP13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/BlanchetteBP13
Jasmin Christian Blanchette, Sascha Böhme, Lawrence C. Paulson:
Extending Sledgehammer with SMT Solvers. J. Autom. Reason. 51(1): 109-128 (2013)
[j4]
- view
  authority control:
- export record
  dblp key:
  - journals/sqj/Blanchette13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/sqj/Blanchette13
Jasmin Christian Blanchette:
Relational analysis of (co)inductive predicates, (co)algebraic datatypes, and (co)recursive functions. Softw. Qual. J. 21(1): 101-126 (2013)
[c19]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/cade/Blanchette13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/Blanchette13
Jasmin Christian Blanchette:
Redirecting Proofs by Contradiction. PxTP@CADE 2013: 11-26
[c18]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/cade/SmolkaB13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/SmolkaB13
Steffen Juilf Smolka, Jasmin Christian Blanchette:
Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs. PxTP@CADE 2013: 117-132
[c17]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/BlanchetteP13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/BlanchetteP13
Jasmin Christian Blanchette, Andrei Paskevich:
TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism. CADE 2013: 414-420
[c16]
- view
  authority control:
- export record
  dblp key:
  - conf/frocos/Blanchette013
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/frocos/Blanchette013
Jasmin Christian Blanchette, Andrei Popescu:
Mechanizing the Metatheory of Sledgehammer. FroCos 2013: 245-260
[c15]
- view
  authority control:
- export record
  dblp key:
  - conf/itp/KuhlweinBKU13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/KuhlweinBKU13
Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, Josef Urban:
MaSh: Machine Learning for Sledgehammer. ITP 2013: 35-50
[c14]
- view
  authority control:
- export record
  dblp key:
  - conf/tacas/BlanchetteBPS13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/BlanchetteBPS13
Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, Nicholas Smallbone:
Encoding Monomorphic and Polymorphic Types. TACAS 2013: 493-507
[e1]
- view
- export record
  dblp key:
  - conf/cade/2013pxtp
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/2013pxtp
Jasmin Christian Blanchette, Josef Urban:
Third International Workshop on Proof Exchange for Theorem Proving, PxTP 2013, Lake Placid, NY, USA, June 9-10, 2013. EPiC Series in Computing 14, EasyChair 2013 [contents]
2012
[b3]
- view
  - electronic edition @ nbn-resolving.org
  - no references & citations available
  authority control:
- export record
  dblp key:
  - phd/dnb/Blanchette12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/phd/dnb/Blanchette12
Jasmin Christian Blanchette:
Automatic proofs and refutations for higher-order logic. Technical University Munich, 2012, pp. 1-173
[c13]
- view
  authority control:
- export record
  dblp key:
  - conf/itp/BlanchettePWW12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/BlanchettePWW12
Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand, Christoph Weidenbach:
More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification. ITP 2012: 345-360
[c12]
- view
  authority control:
- export record
  dblp key:
  - conf/lics/TraytelPB12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lics/TraytelPB12
Dmitriy Traytel, Andrei Popescu, Jasmin Christian Blanchette:
Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving. LICS 2012: 596-605
2011
[j3]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/BlanchetteK11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/BlanchetteK11
Jasmin Christian Blanchette, Alexander Krauss:
Monotonicity Inference for Higher-Order Formulas. J. Autom. Reason. 47(4): 369-398 (2011)
[c11]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/BlanchetteBP11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/BlanchetteBP11
Jasmin Christian Blanchette, Sascha Böhme, Lawrence C. Paulson:
Extending Sledgehammer with SMT Solvers. CADE 2011: 116-130
[c10]
- view
  authority control:
- export record
  dblp key:
  - conf/frocos/BlanchetteBN11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/frocos/BlanchetteBN11
Jasmin Christian Blanchette, Lukas Bulwahn, Tobias Nipkow:
Automatic Proof and Disproof in Isabelle/HOL. FroCoS 2011: 12-27
[c9]
- view
  authority control:
- export record
  dblp key:
  - conf/ppdp/BlanchetteWBOS11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/ppdp/BlanchetteWBOS11
Jasmin Christian Blanchette, Tjark Weber, Mark Batty, Scott Owens, Susmit Sarkar:
Nitpicking C++ concurrency. PPDP 2011: 113-124
2010
[c8]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/BlanchetteK10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/BlanchetteK10
Jasmin Christian Blanchette, Alexander Krauss:
Monotonicity Inference for Higher-Order Formulas. IJCAR 2010: 91-106
[c7]
- view
  authority control:
- export record
  dblp key:
  - conf/itp/BlanchetteN10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/BlanchetteN10
Jasmin Christian Blanchette, Tobias Nipkow:
Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. ITP 2010: 131-146
[c6]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/lpar/PaulsonB10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lpar/PaulsonB10
Lawrence C. Paulson, Jasmin Christian Blanchette:
Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers. IWIL@LPAR 2010: 1-11
[c5]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/lpar/Blanchette10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lpar/Blanchette10
Jasmin Christian Blanchette:
Nitpick: A Counterexample Generator for Isabelle/HOL Based on the Relational Model Finder Kodkod. LPAR short papers(Yogyakarta) 2010: 20-25
[c4]
- view
  authority control:
- export record
  dblp key:
  - conf/lpar/BlanchetteC10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lpar/BlanchetteC10
Jasmin Christian Blanchette, Koen Claessen:
Generating Counterexamples for Structural Inductions by Exploiting Nonstandard Models. LPAR (Yogyakarta) 2010: 127-141
[c3]
- view
  authority control:
- export record
  dblp key:
  - conf/tap/Blanchette10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tap/Blanchette10
Jasmin Christian Blanchette:
Relational Analysis of (Co)inductive Predicates, (Co)algebraic Datatypes, and (Co)recursive Functions. TAP@TOOLS 2010: 117-134

2000 – 2009

see FAQ

What is the meaning of the colors in the publication lists?

2009
[j2]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/Blanchette09
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/Blanchette09
Jasmin Christian Blanchette:
Proof Pearl: Mechanizing the Textbook Proof of Huffman's Algorithm. J. Autom. Reason. 43(1): 1-18 (2009)
2008
[b2]
- no documents available
  - no references & citations available
- export record
  dblp key:
  - books/daglib/0030030
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/books/daglib/0030030
Jasmin Blanchette, Mark Summerfield:
C++ GUI Programming with Qt 4, 2nd Edition. Pearson Education 2008, ISBN 978-0-13-235416-5, pp. I-XXI, 1-718
[j1]
- view
  - electronic edition @ isa-afp.org (open access)
  - no references & citations available
- export record
  dblp key:
  - journals/afp/Blanchette08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/afp/Blanchette08
Jasmin Christian Blanchette:
The Textbook Proof of Huffman's Algorithm. Arch. Formal Proofs 2008 (2008)
[c2]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/entcs/JohnsenBKO09
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/entcs/JohnsenBKO09
Einar Broch Johnsen, Jasmin Christian Blanchette, Marcel Kyas, Olaf Owe:
Intra-Object versus Inter-Object: Concurrency and Reasoning in Creol. TTSS 2008: 89-103
2007
[c1]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/entcs/BlanchetteO08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/entcs/BlanchetteO08
Jasmin Christian Blanchette, Olaf Owe:
An Open System Operational Semantics for an Object-Oriented and Component-Based Language. FACS 2007: 151-169
2006
[b1]
- view
  - no references & citations available
  authority control:
- export record
  dblp key:
  - books/lib/BlanchetteS06
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/books/lib/BlanchetteS06
Jasmin Christian Blanchette, Mark Summerfield:
C++ GUI programming with Qt 4. Prentice Hall 2006, ISBN 0131872494, pp. I-XVII, 1-537

Coauthor Index

see FAQ

manage site settings

To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.