Programming with proofs and explicit contexts
- 15 July 2008
- conference paper
- conference paper
- Published by Association for Computing Machinery (ACM)
- p. 163-173
- https://doi.org/10.1145/1389449.1389469
Abstract
This paper explores a new point in the design space of functional programming: functional programming with dependently-typed higher-order data structures described in the logical framework LF. This allows us to program with proofs as higher-order data. We present a decidable bidirectional type system that distinguishes between dependently-typed data and computations. To support reasoning about open data, our foundation makes contexts explicit. This provides us with a concise characterization of open data, which is crucial to elegantly describe proofs. In addition, we present an operational semantics for this language based on higherorder pattern matching for dependently typed objects. Based on this development, we prove progress and preservationKeywords
This publication has 15 references indexed in Scilit:
- Contextual modal type theoryACM Transactions on Computational Logic, 2008
- A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutionsPublished by Association for Computing Machinery (ACM) ,2008
- Simple unification-based type inference for GADTsPublished by Association for Computing Machinery (ACM) ,2006
- The $\nabla$ -Calculus. Functional Programming with Higher-Order EncodingsLecture Notes in Computer Science, 2005
- The view from the leftJournal of Functional Programming, 2004
- FreshMLPublished by Association for Computing Machinery (ACM) ,2003
- Optimizing Higher-Order Pattern UnificationLecture Notes in Computer Science, 2003
- Recursion over objects of functional typeMathematical Structures in Computer Science, 2001
- A framework for defining logicsJournal of the ACM, 1993
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple UnificationJournal of Logic and Computation, 1991