Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice
Karl Crary, Marino Miculan

TL;DR
This workshop volume compiles research on logical frameworks, meta-languages, and their applications in programming language design, theorem proving, and formal reasoning, highlighting recent advances and practical implementations.
Contribution
It presents the latest developments in automation, proof assistants, and encoding techniques within logical frameworks, advancing both theoretical understanding and practical tools.
Findings
Enhanced methods for encoding variable binding and fresh name generation
Case studies demonstrating meta-programming applications
Mechanization of language and calculus descriptions
Abstract
Type theories, logical frameworks and meta-languages form a common foundation for designing, implementing, and reasoning about formal languages and their semantics. They are central to the design of modern programming languages, certified software, and domain specific logics. More generally, they continue to influence applications in many areas in mathematics, logic and computer science. The Logical Frameworks and Meta-languages: Theory and Practice workshop aims to bring together designers, implementers, and practitioners working on these areas, and in particular about: the automation and implementation of the meta-theory of programming languages and related calculi; the design of proof assistants, automated theorem provers, and formal digital libraries building upon logical framework technology; theoretical and practical issues concerning the encoding of variable binding and fresh…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
