Travelled to:1 × Austria
1 × Canada
1 × Croatia
1 × Denmark
1 × Germany
1 × Italy
1 × Poland
1 × Spain
1 × USA
2 × United Kingdom
Collaborated with:D.Traytel A.Popescu A.Reynolds U.Waldmann S.Böhme A.Paskevich A.Krauss ∅ S.Cruanes A.P.0001 L.C.Paulson M.Fleury C.Weidenbach H.Barbosa P.Fontaine N.Peltier S.Robillard N.Smallbone C.Tinelli H.Becker D.Wand A.Bentkamp A.Schlichtkrull Lorenzo Gheri T.Weber M.Batty S.Owens S.Sarkar A.Bouzy A.Lochbihler L.Hupel T.Nipkow L.Noschinski
Talks about:order (7) datatyp (5) higher (4) foundat (3) solver (3) proof (3) logic (3) smt (3) superposit (2) polymorph (2)
Person: Jasmin Christian Blanchette
DBLP: Blanchette:Jasmin_Christian
Facilitated 1 volumes:
EdContributed to:
2015
2015
2015
20142013
2013
20122011
2011201020102017201620172018
2014
2019Wrote 21 papers:
- CADE-2015-ReynoldsB #data type #smt
- A Decision Procedure for (Co)datatypes in SMT Solvers (AR, JCB), pp. 197–213.
- ESOP-2015-Blanchette0T #data type
- Witnessing (Co)datatypes (JCB, AP, DT), pp. 359–382.
- ICFP-2015-Blanchette0T #perspective #proving #recursion
- Foundational extensible corecursion: a proof assistant perspective (JCB, AP, DT), pp. 192–204.
- IJCAR-2014-Blanchette0T #induction #logic
- Unified Classical Logic Completeness — A Coinductive Pearl (JCB, AP, DT), pp. 46–60.
- CADE-2013-BlanchetteP #first-order #morphism #named #polymorphism
- TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism (JCB, AP), pp. 414–420.
- TACAS-2013-BlanchetteBPS #encoding #polymorphism
- Encoding Monomorphic and Polymorphic Types (JCB, SB, AP, NS), pp. 493–507.
- LICS-2012-TraytelPB #category theory #composition #data type #higher-order #logic #proving #theorem proving
- Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving (DT, AP, JCB), pp. 596–605.
- CADE-2011-BlanchetteBP #smt
- Extending Sledgehammer with SMT Solvers (JCB, SB, LCP), pp. 116–130.
- PPDP-2011-BlanchetteWBOS #c++ #concurrent
- Nitpicking C++ concurrency (JCB, TW, MB, SO, SS), pp. 113–124.
- IJCAR-2010-BlanchetteK #higher-order
- Monotonicity Inference for Higher-Order Formulas (JCB, AK), pp. 91–106.
- TAP-2010-Blanchette #algebra #analysis #data type #induction #recursion #relational
- Relational Analysis of (Co)inductive Predicates, (Co)algebraic Datatypes, and (Co)recursive Functions (JCB), pp. 117–134.
- ESOP-2017-BlanchetteBL0T #implementation #proving #recursion
- Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants (JCB, AB, AL, AP0, DT), pp. 111–140.
- IJCAR-2016-BlanchetteFW #framework #satisfiability
- A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality (JCB, MF, CW), pp. 25–44.
- IJCAR-2016-ReynoldsBCT #recursion #smt
- Model Finding for Recursive Functions in SMT (AR, JCB, SC, CT), pp. 133–151.
- CADE-2017-BarbosaBF #fine-grained #proving #scalability
- Scalable Fine-Grained Proofs for Formula Processing (HB, JCB, PF), pp. 398–412.
- CADE-2017-BeckerBWW #higher-order
- A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms (HB, JCB, UW, DW), pp. 432–453.
- IJCAR-2018-BentkampBCW #higher-order #logic
- Superposition for Lambda-Free Higher-Order Logic (AB, JCB, SC, UW), pp. 28–46.
- IJCAR-2018-BlanchettePR #data type
- Superposition with Datatypes and Codatatypes (JCB, NP, SR), pp. 370–387.
- IJCAR-2018-SchlichtkrullBT #formal method #order #proving
- Formalizing Bachmair and Ganzinger's Ordered Resolution Prover (AS, JCB, DT, UW), pp. 89–107.
- Haskell-2014-BlanchetteHNNT #case study #experience #haskell
- Experience report: the next 1100 Haskell programmers (JCB, LH, TN, LN, DT), pp. 25–30.
- POPL-2019-BlanchetteGPT #bound
- Bindings as bounded natural functors (JCB, LG, AP0, DT), p. 34.