Christian Urban

J. Autom. Reason., September, 2023

POSIX Lexing with Bitcoded Derivatives.

[BibT_eX]

[DOI]

Chengsong Tan

Proceedings of the 14th International Conference on Interactive Theorem Proving, 2023

2020

Priority Inheritance Protocol Proved Correct.

[BibT_eX]

[DOI]

J. Autom. Reason., 2020

2019

Selected Extended Papers of ITP 2015: Preface.

[BibT_eX]

[DOI]

J. Autom. Reason., 2019

Universal Turing Machine.

[BibT_eX]

[DOI]

Jian Xu

Sebastiaan J. C. Joosten

Arch. Formal Proofs, 2019

2017

Modelling Homogeneous Generative Meta-Programming.

[BibT_eX]

[DOI]

Martin Berger

Laurence Tratt

Proceedings of the 31st European Conference on Object-Oriented Programming, 2017

2016

POSIX Lexing with Derivatives of Regular Expressions.

[BibT_eX]

[DOI]

Fahad Ausaf

Roy Dyckhoff

Arch. Formal Proofs, 2016

POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl).

[BibT_eX]

[DOI]

Fahad Ausaf

Roy Dyckhoff

Proceedings of the Interactive Theorem Proving - 7th International Conference, 2016

2014

A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions.

[BibT_eX]

[DOI]

J. Autom. Reason., 2014

2013

Mechanising Turing Machines and Computability Theory in Isabelle/HOL.

[BibT_eX]

[DOI]

Jian Xu

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

A Formal Model and Correctness Proof for an Access Control Policy Framework.

[BibT_eX]

[DOI]

Proceedings of the Certified Programs and Proofs - Third International Conference, 2013

2012

Preface: Theory and Applications of Abstraction, Substitution and Naming.

[BibT_eX]

[DOI]

Maribel Fernández

J. Autom. Reason., 2012

General Bindings and Alpha-Equivalence in Nominal Isabelle

[BibT_eX]

[DOI]

Cezary Kaliszyk

Log. Methods Comput. Sci., 2012

2011

Mechanizing the metatheory of LF.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2011

The Myhill-Nerode Theorem Based on Regular Expressions.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2011

Quotients revisited for Isabelle/HOL.

[BibT_eX]

[DOI]

Cezary Kaliszyk

Proceedings of the 2011 ACM Symposium on Applied Computing (SAC), TaiChung, Taiwan, March 21, 2011

A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl).

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - Second International Conference, 2011

Mechanizing the Metatheory of mini-XQuery.

[BibT_eX]

[DOI]

Proceedings of the Certified Programs and Proofs - First International Conference, 2011

2010

Nominal Unification Revisited

[BibT_eX]

[DOI]

Proceedings of the Proceedings 24th International Workshop on Unification, 2010

A New Foundation for Nominal Isabelle.

[BibT_eX]

[DOI]

Brian Huffman

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

2008

Nominal logic programming.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2008

Nominal Techniques in Isabelle/HOL.

[BibT_eX]

[DOI]

J. Autom. Reason., 2008

Formal SOS-Proofs for the Lambda-Calculus.

[BibT_eX]

[DOI]

Julien Narboux

Proceedings of the Third Workshop on Logical and Semantic Frameworks with Applications, 2008

Preface.

[BibT_eX]

[DOI]

Andreas Abel

Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, 2008

Nominal Inversion Principles.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008

Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof.

[BibT_eX]

[DOI]

Bozhi Zhu

Proceedings of the Rewriting Techniques and Applications, 19th International Conference, 2008

Mechanising a Proof of Craig's Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle.

[BibT_eX]

[DOI]

Peter Chapman

James McKinna

Proceedings of the Intelligent Computer Mathematics, 9th International Conference, 2008

2007

Formalising in Nominal Isabelle Crary's Completeness Proof for Equivalence Checking.

[BibT_eX]

[DOI]

Julien Narboux

Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2007

Barendregt's Variable Convention in Rule Inductions.

[BibT_eX]

[DOI]

Michael Norrish

Proceedings of the Automated Deduction, 2007

2006

Categorical proof theory of classical propositional calculus.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2006

A Head-to-Head Comparison of de Bruijn Indices and Names.

[BibT_eX]

[DOI]

Proceedings of the First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2006

A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

2005

Avoiding Equivariance in Alpha-Prolog.

[BibT_eX]

[DOI]

Proceedings of the Typed Lambda Calculi and Applications, 7th International Conference, 2005

A formal treatment of the barendregt variable convention in rule inductions.

[BibT_eX]

[DOI]

Michael Norrish

Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2005

Nominal Techniques in Isabelle/HOL.

[BibT_eX]

[DOI]

Christine Tasson

Proceedings of the Automated Deduction, 2005

2004

Nominal unification.

[BibT_eX]

[DOI]

Andrew M. Pitts

Murdoch Gabbay

Theor. Comput. Sci., 2004

alpha-Prolog: A Logic Programming Language with Names, Binding and a-Equivalence.

[BibT_eX]

[DOI]

Proceedings of the Logic Programming, 20th International Conference, 2004

2003

Strong Normalization of Herbelin's Explicit Substitution Calculus with Substitution Propagation.

[BibT_eX]

[DOI]

Roy Dyckhoff

J. Log. Comput., 2003

Nominal Unificaiton.

[BibT_eX]

[DOI]

Andrew M. Pitts

Murdoch Gabbay

Proceedings of the Computer Science Logic, 17th International Workshop, 2003

2001

Strong Normalisation of Cut-Elimination in Classical Logic.

[BibT_eX]

[DOI]

Gavin M. Bierman

Fundam. Informaticae, 2001

Strong Normalisation for a Gentzen-like Cut-Elimination Procedure.

[BibT_eX]

[DOI]

Proceedings of the Typed Lambda Calculi and Applications, 5th International Conference, 2001

1998

Implementation of Proof Search in the Imperative Programming Language Pizza.

[BibT_eX]

[DOI]