Adelfa: a system for reasoning about LF specifications

DOI10.4204/EPTCS.337.8MaRDI QIDQ6940473zbMATH OpenFDO

Authors Mary Southern, Gopalan Nadathur

Publication date 19 August 2025

Copyright license Creative Commons license

Full work available at URL https://doi.org/10.4204/EPTCS.337.8

Mathematics Subject Classification ID

Logic in computer science (03B70) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A framework for defining logics
• A logic for reasoning about generic judgments
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• A two-level logic approach to reasoning about typed specification languages
• Abella: a system for reasoning about relational specifications
• Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
• Contextual modal type theory
• Encoding a dependent-type λ-calculus in a logic programming language
• Logic Programming
• Mechanizing metatheory in a logical framework
• Nominal abstraction
• Theorem Proving in Higher Order Logics
• Unification under a mixed prefix

This page was built for publication: Adelfa: a system for reasoning about LF specifications

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6940473)