|  | 
|  | 
| | PxTP 2013: Author Index| Author | Papers | 
|---|
 | B |  | Benzmüller, Christoph | LEO-II Version 1.5 |  | Blanchette, Jasmin Christian | Redirecting Proofs by Contradiction Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs
 |  | Brown, Chad | From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction |  | Burel, Guillaume | A Shallow Embedding of Resolution and Superposition Proofs into the $\lambda\Pi$-Calculus Modulo |  | C |  | Chihani, Zakaria | Checking Foundational Proof Certificates for First-Order Logic (Extended Abstract) |  | F |  | Felty, Amy | Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs |  | H |  | Habli, Nada | Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs |  | Hales, Thomas | External Tools for the Formal Proof of the Kepler Conjecture |  | K |  | Kaliszyk, Cezary | Initial Experiments on Deriving a Complete HOL Simplification Set Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution
 |  | Keller, Chantal | Extended Resolution as Certificates for Propositional Logic |  | Kumar, Ramana | Challenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4 |  | M |  | Miller, Dale | Checking Foundational Proof Certificates for First-Order Logic (Extended Abstract) |  | R |  | Renaud, Fabien | Checking Foundational Proof Certificates for First-Order Logic (Extended Abstract) |  | Rizkallah, Christine | From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction |  | S |  | Smolka, Steffen Juilf | Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs |  | Sternagel, Thomas | Initial Experiments on Deriving a Complete HOL Simplification Set |  | Sultana, Nik | LEO-II Version 1.5 |  | U |  | Urban, Josef | Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution | 
 | 
 | 
|