32 papers:
SAC-2015-Buday #formal method- Formalising the SECD machine with nominal Isabelle (GB), pp. 1823–1824.
CADE-2015-MaricJM #correctness #higher-order #proving #using- Proving Correctness of a KRK Chess Endgame Strategy by Using Isabelle/HOL and Z3 (FM, PJ, MM), pp. 256–271.
SEFM-2014-ArmstrongGS #higher-order #lightweight #tool support #verification- Lightweight Program Construction and Verification Tools in Isabelle/HOL (AA, VBFG, GS), pp. 5–19.
ESOP-2011-UrbanK- General Bindings and α-Equivalence in Nominal Isabelle (CU, CK), pp. 480–500.
- SAC-2011-KaliszykU #higher-order
- Quotients revisited for Isabelle/HOL (CK, CU), pp. 1639–1644.
FoSSaCS-2010-PopescuG #algebra #formal method #incremental #induction #process- Incremental Pattern-Based Coinduction for Process Algebra and Its Isabelle Formalization (AP, ELG), pp. 109–127.
PLEASE-2010-KammullerRR #higher-order #variability- Feature link propagation across variability representations with Isabelle/HOL (FK, AR, MOR), pp. 48–53.
PPDP-2009-KaiserL #higher-order #traversal- An Isabelle/HOL-based model of stratego-like traversal strategies (MK, RL), pp. 93–104.
CAV-2008-MeikleF #approach #proving #verification- Prover’s Palette: A User-Centric Approach to Verification with Isabelle and QEPCAD-B (LIM, JDF), pp. 309–313.
IJCAR-2006-McLaughlin #higher-order- An Interpretation of Isabelle/HOL in HOL Light (SM), pp. 192–204.
- IJCAR-2006-ObuaS #higher-order
- Importing HOL into Isabelle/HOL (SO, SS), pp. 298–302.
- IJCAR-2006-UrbanB #combinator #data type #higher-order #recursion
- A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL (CU, SB), pp. 498–512.
FASE-2005-HausmannMS #higher-order #induction- Iterative Circular Coinduction for CoCasl in Isabelle/HOL (DH, TM, LS), pp. 341–356.
- SEFM-2005-BlechGG #higher-order #verification
- Formal Verification of Dead Code Elimination in Isabelle/HOL (JOB, LG, SG), pp. 200–209.
COCV-J-2005-BlechGLM #code generation #comparison #correctness #higher-order #optimisation #proving- Optimizing Code Generation from SSA Form: A Comparison Between Two Formal Correctness Proofs in Isabelle/HOL (JOB, SG, JL, SM), pp. 33–51.
- CADE-2005-UrbanT #higher-order
- Nominal Techniques in Isabelle/HOL (CU, CT), pp. 38–53.
- SEFM-2004-BerghoferN #higher-order #random testing #testing
- Random Testing in Isabelle/HOL (SB, TN), pp. 230–239.
- IJCAR-2004-AvigadD #formal method #higher-order
- Formalizing O Notation in Isabelle/HOL (JA, KD), pp. 357–371.
- ESOP-2003-Nieto #higher-order
- The Rely-Guarantee Method in Isabelle/HOL (LPN), pp. 348–362.
LOPSTR-2003-LehmannL #generative #induction #proving #theorem proving #using- Inductive Theorem Proving by Program Specialisation: Generating Proofs for Isabelle Using Ecce (HL, ML), pp. 1–19.
- CADE-2003-DixonF #named #prototype #proving #theorem proving
- IsaPlanner: A Prototype Proof Planner in Isabelle (LD, JDF), pp. 279–283.
- CADE-2002-Strecker #compilation #java #verification
- Formal Verification of a Java Compiler in Isabelle (MS), pp. 63–77.
- FoSSaCS-2001-RocklHB #formal method #higher-order #induction #syntax #π-calculus
- Higher-Order Abstract Syntax with Induction in Isabelle/HOL: Formalizing the π-Calculus and Mechanizing the Theory of Contexts (CR, DH, SB), pp. 364–378.
- CADE-2000-Kammuller #composition #reasoning
- Modular Reasoning in Isabelle (FK), pp. 99–114.
- FASE-1999-NipkowN #higher-order
- Owicki/Gries in Isabelle/HOL (TN, LPN), pp. 188–203.
TACAS-1999-Pusch #bytecode #higher-order #java #proving #specification #verification- Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL (CP), pp. 89–103.
FME-1997-TejW #csp #higher-order- A Corrected Failure Divergence Model for CSP in Isabelle/HOL (HT, BW), pp. 318–337.
- CADE-1997-OzolsCE #named
- XIsabelle: A System Description (MAO, AC, KAE), pp. 400–403.
- CADE-1996-Nipkow #higher-order #proving
- More Church-Rosser Proofs (in Isabelle/HOL) (TN), pp. 733–747.
- CADE-1996-Rasmussen #ruby
- An Embedding of Ruby in Isabelle (OR), pp. 186–200.
ICLP-1994-Basin- IsaWhelk Interpreted in Isabelle (DAB), p. 741.
- CADE-1988-Paulson #named #proving #theorem proving
- Isabelle: The Next Seven Hundred Theorem Provers (LCP), pp. 772–773.
