Author of the publication

Strong Normalisation of Cut-Elimination in Classical Logic.

, and . TLCA, volume 1581 of Lecture Notes in Computer Science, page 365-380. Springer, (1999)

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

Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof., and . RTA, volume 5117 of Lecture Notes in Computer Science, page 409-424. Springer, (2008)A Formal Model and Correctness Proof for an Access Control Policy Framework., , and . CPP, volume 8307 of Lecture Notes in Computer Science, page 292-307. Springer, (2013)Strong Normalisation of Cut-Elimination in Classical Logic., and . Fundam. Informaticae, 45 (1-2): 123-155 (2001)Formal SOS-Proofs for the Lambda-Calculus., and . LSFA, volume 247 of Electronic Notes in Theoretical Computer Science, page 139-155. Elsevier, (2008)A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl)., , and . ITP, volume 6898 of Lecture Notes in Computer Science, page 341-356. Springer, (2011)A New Foundation for Nominal Isabelle., and . ITP, volume 6172 of Lecture Notes in Computer Science, page 35-50. Springer, (2010)Quotients revisited for Isabelle/HOL., and . SAC, page 1639-1644. ACM, (2011)Strong Normalisation of Cut-Elimination in Classical Logic., and . TLCA, volume 1581 of Lecture Notes in Computer Science, page 365-380. Springer, (1999)Nominal Unificaiton., , and . CSL, volume 2803 of Lecture Notes in Computer Science, page 513-527. Springer, (2003)POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl)., , and . ITP, volume 9807 of Lecture Notes in Computer Science, page 69-86. Springer, (2016)