A Coverage Checking Algorithm for LF

DOI10.1007/10930755_8zbMath1279.68295OpenAlexW1480580285MaRDI QIDQ3559763

Carsten Schuermann, 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

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

Related Items

The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey, Verifying termination and reduction properties about higher-order logic programs, Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax, Case Analysis of Higher-Order Data, A New Elimination Rule for the Calculus of Inductive Constructions, Functional Programming With Higher-order Abstract Syntax and Explicit Substitutions, Hybridizing a Logical Framework, Normalization for the Simply-Typed Lambda-Calculus in Twelf

Uses Software

• Coq
• Twelf
• Delphin