BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
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 DBLP: Blanchette:Jasmin_Christian

Facilitated 1 volumes:

TAP 2015Ed

Contributed to:

CADE 20152015
ESOP 20152015
ICFP 20152015
IJCAR 20142014
CADE 20132013
TACAS 20132013
LICS 20122012
CADE 20112011
PPDP 20112011
IJCAR 20102010
TAP 20102010
ESOP 20172017
IJCAR 20162016
CADE 20172017
IJCAR 20182018
Haskell 20142014
POPL 20192019

Wrote 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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.