A coverage checking algorithm for LF

DOI10.1007/10930755_8MaRDI QIDQ3559763zbMATH OpenOpenAlexFDO

Authors Carsten Schürmann, Frank Pfenning

Publication date 7 May 2010

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://figshare.com/articles/journal_contribution/A_Coverage_Checking_Algorithm_for_LF/6587336

zbMATH Keywords

logical framework LF

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Functional programming and lambda calculus (68N18)

Recommendations

• Case analysis of higher-order data
• Theorem Proving in Higher Order Logics
• Mechanizing the metatheory of LF
• On equivalence and canonical forms in the LF type theory
• Subtyping dependent types

Cited in

(10)

• Case analysis of higher-order data
• Functional programming with higher-order abstract syntax and explicit substitutions
• Hybridizing a logical framework
• Normalization for the simply-typed lambda-calculus in Twelf
• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• A New Elimination Rule for the Calculus of Inductive Constructions
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• Theorem Proving in Higher Order Logics
• A saturation-based unification algorithm for higher-order rational patterns
• Verifying termination and reduction properties about higher-order logic programs

Describes a project that uses

Uses Software

• Coq
• Twelf
• Delphin

This page was built for publication: A coverage checking algorithm for LF

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