Case analysis of higher-order data

DOI10.1016/J.ENTCS.2008.12.117zbMATH Open1337.68058OpenAlexW1969412609MaRDI QIDQ2804942FDOQ2804942

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

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

zbMATH Keywords

higher-order abstract syntaxcoverage checking

Mathematics Subject Classification ID

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

Cites Work

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

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
• A coverage checking algorithm for LF
• Programming inductive proofs. A new approach based on contextual types
• Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)

Uses Software

• Twelf
• Bedwyr

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)