Output details
11 - Computer Science and Informatics
King's College London
Return to search
Output 0 of 0 in the submission
Article title
General Bindings and Alpha-Equivalence in Nominal Isabelle
Type
D - Journal article
Title of journal
Logical methods in computer science
Article number
14
Volume number
8
Issue number
2
First page of article
-
ISSN of journal
1860-5974
Year of publication
2012
Number of additional authors
1
Additional information
<07> This is the first paper that describes a fully automated reasoning infrastructure for general binders. It is already used by the group of Prof. Joachim Parrow (Uppsala) in order to formalise results about calculi for concurrency and by Prof. Lawrence Paulson (from Cambridge) in order to formalise Goedel's incompleteness theorems. A group in Karlsruhe uses this work to verify the correctness of Launchbury's natural semantics for lazy evaluation. All formalisations are part of the Archive of Formal Proofs.
Interdisciplinary
-
Cross-referral requested
-
Research group
D - Software Modelling and Applied Logic
Citation count
1
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-
