Case analysis of higher-order data

DOI10.1016/J.ENTCS.2008.12.117MaRDI QIDQ2804942zbMATH OpenOpenAlexFDO

Authors Joshua Dunfield, Brigitte Pientka

Publication date 6 May 2016

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2008.12.117

zbMATH Keywords

higher-order abstract syntaxcoverage checking

Mathematics Subject Classification ID

Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Recommendations

• A coverage checking algorithm for LF
• scientific article; zbMATH DE number 2185657
• Higher-order abstract syntax in type theory
• The theory of contexts for first order and higher order abstract syntax
• Reasoning with higher-order abstract syntax and contexts: a comparison

Cites work

• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• A coverage checking algorithm for LF
• A framework for defining logics
• A meta linear logical framework
• A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
• Contextual modal type theory
• Logic Programming
• Practical Programming with Higher-Order Encodings and Dependent Types
• Typed Lambda Calculi and Applications
• Types for Proofs and Programs

Cited in

(6)

• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• Case studies in data analysis
• Inductive beluga: programming proofs
• Programming inductive proofs. A new approach based on contextual types
• A coverage checking algorithm for LF
• Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)

Describes a project that uses

Uses Software

• Bedwyr
• Twelf

This page was built for publication: Case analysis of higher-order data

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