Case Analysis of Higher-Order Data
From MaRDI portal
Publication:2804942
DOI10.1016/j.entcs.2008.12.117zbMath1337.68058OpenAlexW1969412609MaRDI QIDQ2804942
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (4)
The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey ⋮ Inductive Beluga: Programming Proofs ⋮ Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description) ⋮ Programming Inductive Proofs
Uses Software
Cites Work
- A Meta Linear Logical Framework
- A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
- A Coverage Checking Algorithm for LF
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- A framework for defining logics
- Logic Programming
- Contextual modal type theory
- Practical Programming with Higher-Order Encodings and Dependent Types
- Typed Lambda Calculi and Applications
- Types for Proofs and Programs
This page was built for publication: Case Analysis of Higher-Order Data
