Abstract
Higher-order abstract syntax (HOAS) refers to the technique of representing variables of an object-language using variables of a meta-language. The standard first-order alternatives force the programmer to deal with superficial concerns such as substitutions, whose implementation is often routine, tedious, and error-prone. In this paper, we describe the underlying calculus of Delphin. Delphin is a fully implemented functional-programming language supporting reasoning over higher-order encodings and dependent types, while maintaining the benefits of HOAS. More specifically, just as representations utilizing HOAS free the programmer from concerns of handling explicit contexts and substitutions, our system permits programming over such encodings without making these constructs explicit, leading to concise and elegant programs. To this end our system distinguishes bindings of variables intended for instantiation from those that will remain uninstantiated, utilizing a variation of Miller and Tiu’s \(\nabla\)-quantifier [1].
This research has been funded by NSF grants CCR-0325808 and CCR-0133502.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Miller, D., Tiu, A.: A proof theory for generic judgments. ACM Trans. on Computational Logic 6(4), 749–783 (2005)
Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the Association for Computing Machinery 40(1), 143–184 (1993)
Poswolsky, A., Schürmann, C.: Extended report on Delphin: A functional programming language with higher-order encodings and dependent types. Technical Report YALEU/DCS/TR-1375, Yale University (2007)
Schürmann, C., Pfenning, F.: A coverage checking algorithm for LF. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, Springer, Heidelberg (2003)
Dowek, G., Hardin, T., Kirchner, C., Pfenning, F.: Unification via explicit substitutions: The case of higher-order patterns. Rapport de Recherche 3591, INRIA (December 1998) Preliminary version appeared at JICSLP 1996 (1996)
Schürmann, C., Poswolsky, A., Sarnat, J.: The \(\nabla\)-calculus. Functional programming with higher-order encodings. In: Typed Lambda Calculus and Applications, TLCA (2005)
Pientka, B.: A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In: Principles of Programming Languages, POPL (2008)
Gabbay, M., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Aspects Computing 13(3-5), 341–363 (2002)
Pottier, F.: Static name control for FreshML. In: Twenty-Second Annual IEEE Symposium on Logic In Computer Science (LICS 2007), Wroclaw, Poland (July 2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Poswolsky, A., Schürmann, C. (2008). Practical Programming with Higher-Order Encodings and Dependent Types. In: Drossopoulou, S. (eds) Programming Languages and Systems. ESOP 2008. Lecture Notes in Computer Science, vol 4960. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78739-6_7
Download citation
DOI: https://doi.org/10.1007/978-3-540-78739-6_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78738-9
Online ISBN: 978-3-540-78739-6
eBook Packages: Computer ScienceComputer Science (R0)