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 × Estonia
1 × Japan
1 × Serbia
1 × Sweden
1 × United Kingdom
2 × Austria
2 × Denmark
7 × USA
Collaborated with:
D.L.Dill C.W.Barrett I.Wehrman E.M.Westbrook P.Fu J.Carette L.Tan G.Sutcliffe C.Tinelli G.Kimmell R.E.H.Omar L.M.d.Moura D.Wu A.W.Appel D.Oe C.Oliver K.Clancy J.R.Levitt R.Besand J.C.Brodman J.Hseu B.Kinnersley G.T.Leavens J.Abrial D.S.Batory M.J.Butler A.Coglio K.Fisler E.C.R.Hehner C.B.Jones D.Miller S.L.P.Jones M.Sitaraman D.R.Smith
Talks about:
type (5) checker (3) proof (3) framework (2) procedur (2) function (2) satisfi (2) languag (2) theori (2) modern (2)

Person: Aaron Stump

DBLP DBLP: Stump:Aaron

Contributed to:

IJCAR 20142014
RTA-TLCA 20142014
PEPM 20122012
VMCAI 20122012
RTA 20112011
GPCE 20062006
RTA 20062006
CAV 20052005
ICFP 20052005
RTA 20052005
WRLA 20042005
CADE 20032003
PPDP 20032003
CADE 20022002
CAV 20022002
LICS 20012001
CADE 20002000

Wrote 18 papers:

IJCAR-2014-StumpST #framework #logic #named
StarExec: A Cross-Community Infrastructure for Logic Solving (AS, GS, CT), pp. 367–373.
RTA-TLCA-2014-FuS #encoding
Self Types for Dependently Typed λ Encodings (PF, AS), pp. 224–239.
PEPM-2012-CaretteS #towards #type system
Towards typing for small-step direct reflection (JC, AS), pp. 93–96.
VMCAI-2012-OeSOC #named #satisfiability
versat: A Verified Modern SAT Solver (DO, AS, CO, KC), pp. 363–378.
RTA-2011-StumpKO #confluence #problem
Type Preservation as a Confluence Problem (AS, GK, REHO), pp. 345–360.
GPCE-2006-LeavensABBCFHJMJSSS #roadmap #verification
Roadmap for enhanced languages and methods to aid verification (GTL, JRA, DSB, MJB, AC, KF, ECRH, CBJ, DM, SLPJ, MS, DRS, AS), pp. 221–236.
RTA-2006-WehrmanSW #named #termination
Slothrop: Knuth-Bendix Completion with a Modern Termination Checker (IW, AS, EMW), pp. 287–296.
CAV-2005-BarrettMS #contest #modulo theories #named #satisfiability
SMT-COMP: Satisfiability Modulo Theories Competition (CWB, LMdM, AS), pp. 20–23.
ICFP-2005-WestbrookSW #approach #imperative #programming
A language-based approach to functionally correct imperative programming (EMW, AS, IW), pp. 268–279.
RTA-2005-StumpT #algebra #proving #similarity
The Algebra of Equality Proofs (AS, LYT), pp. 469–483.
From Rogue to MicroRogue (AS, RB, JCB, JH, BK), pp. 69–87.
CADE-2003-Stump #set
Subset Types and Partial Functions (AS), pp. 151–165.
PPDP-2003-WuAS #proving
Foundational proof checkers with small witnesses (DW, AWA, AS), pp. 264–274.
CADE-2002-StumpD #framework #logic #performance #proving
Faster Proof Checking in the Edinburgh Logical Framework (AS, DLD), pp. 392–407.
CAV-2002-BarrettDS #first-order #incremental #satisfiability
Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT (CWB, DLD, AS), pp. 236–249.
CAV-2002-StumpBD #named
CVC: A Cooperating Validity Checker (AS, CWB, DLD), pp. 500–504.
LICS-2001-StumpBDL #array
A Decision Procedure for an Extensional Theory of Arrays (AS, CWB, DLD, JRL), pp. 29–37.
CADE-2000-BarrettDS #framework
A Framework for Cooperating Decision Procedures (CWB, DLD, AS), pp. 79–98.

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.