Blogs about: Theorem Proving
Featured Blog
Higher-order abstract syntax with induction in Isabelle/HOL: formalizing the pi-calculus and mechanizing the Theory of Contexts
By Christine Roeckl, Daniel Hirchskoff and Stefan Berghofer, from FOSSACS 2001, available from Christine Roeckl’s website: Higher-order abstract syntax is a natural way to formalize programming … more →
Name binding blog
Higher-order abstract syntax with induction in Isabelle/HOL: formalizing the pi-calculus and mechanizing the Theory of Contexts
Name Binding Admin wrote 1 week ago: By Christine Roeckl, Daniel Hirchskoff and Stefan Berghofer, from FOSSACS 2001, available from Chris … more →
Combining de Bruijn indices and higher-order abstract syntax in Coq
Name Binding Admin wrote 2 weeks ago: Sorry for the long delay in posting any updates. This last week, I was invited to give a talk in Su … more →
Abstracting syntax
Name Binding Admin wrote 4 weeks ago: By Brian Aydemir, Stephan A. Zdancewic and Stephanie Weirich, University of Pennsylvania Technical R … more →
The calculus of nominal inductive constructions
Name Binding Admin wrote 1 month ago: By Edwin Westbrook, Aaron Stump and Evan Austin, from LFMTP 2009, available from Aaron Stump’s … more →
A head-to-head comparison of de Bruijn indices and names
— 5 comments
Name Binding Admin wrote 2 months ago: Stefan Berghofer and Christian Urban, from LFMTP 2006, available from the Nominal Isabelle research … more →
A Machine Program for Theorem-Proving
— 1 comment
dcoetzee wrote 9 months ago: Citation: Davis, M., Logemann, G., and Loveland, D. A machine program for theorem-proving. Communica … more →
Fear, courage, and place in problem solving
— 3 comments
Robert wrote 2 years ago: Sorry for the slowdown in posting. It’s been tremendously busy here lately with hosting our an … more →
DreamProver: A visual theorem prover for "Multiple Form Logic" (etc.) in LPA Win-Prolog 4.6
— 20 comments
omadeon wrote 2 years ago: Image via Wikipedia Visual DreamProver 1.0 is a new theorem-proving program, developed in LPA Win-Pr … more →
A case for proof assistants, and a comparison
atomb wrote 2 years ago: In the last two years or so, I’ve written far too many programming language soundness proofs. … more →
