Author of the publication

A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic.

, and . TPHOLs, volume 3603 of Lecture Notes in Computer Science, page 294-309. Springer, (2005)

Please choose a person to relate this publication to

To differ between persons with the same name, the academic degree and the title of an important publication will be displayed. You can also use the button next to the name to display some publications already assigned to the person.

 

Other publications of authors with the same name

Simple, Efficient, Sound and Complete Combinator Parsing for All Context-Free Grammars, Using an Oracle.. SLE, volume 8706 of Lecture Notes in Computer Science, page 261-281. Springer, (2014)Lem: reusable engineering of real-world semantics., , , , and . ICFP, page 175-188. ACM, (2014)A Rigorous Approach to Networking: TCP, from Implementation to Protocol to Service., , and . FM, volume 5014 of Lecture Notes in Computer Science, page 294-309. Springer, (2008)Craig's Interpolation Theorem formalised and mechanised in Isabelle/HOL. CoRR, (2006)Ramsey's theorem, infinitary version.. Arch. Formal Proofs, (2004)Formal proof development.Rigorous Protocol Design in Practice: An Optical Packet-Switch MAC in HOL., , , , and . ICNP, page 117-126. IEEE Computer Society, (2006)Verifying distributed systems: the operational approach.. POPL, page 429-440. ACM, (2009)Completeness theorem., and . Arch. Formal Proofs, (2004)Formal proof development.Operational Reasoning for Concurrent Caml Programs and Weak Memory Models.. TPHOLs, volume 4732 of Lecture Notes in Computer Science, page 278-293. Springer, (2007)A Rely-Guarantee Proof System for x86-TSO.. VSTTE, volume 6217 of Lecture Notes in Computer Science, page 55-70. Springer, (2010)