Thumbnail
Access Restriction
Open

Author Christian, Jasmin ♦ Andrei, Blanchette ♦ Traytel, Popescu Dmitriy
Source CiteSeerX
Content type Text
File Format PDF
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Modular First-order Logic Completeness ♦ Coinductive Pearl ♦ Gentzen System ♦ Derivation Tree ♦ Isabelle Hol ♦ Lazy Data Structure ♦ Definitional Package ♦ Abstract Property ♦ Classic Result ♦ Concern Simplifies ♦ Concrete Syntax ♦ Isabelle Haskell Code Generator ♦ Codatatypes Help ♦ Inference Rule ♦ Completeness Theorem ♦ Proof Assistant ♦ First-order Logic
Abstract Codatatypes are regrettably absent from many programming languages and proof assistants. We make a case for their usefulness by revisiting a classic result: the completeness theorem for first-order logic established through a Gentzen system. Codatatypes help capture the essence of the proof, which establishes an abstract property of derivation trees independently of the concrete syntax or inference rules. This separation of concerns simplifies the presentation, especially for readers acquainted with lazy data structures. The proof is formalized in Isabelle/HOL and demonstrates the recently introduced definitional package for codatatypes and its integration with Isabelle’s Haskell code generator.
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research
Education Level UG and PG ♦ Career/Technical Study
Publisher Institution Technische Universität München