Abstract
This paper describes a calculus of partial recursive functions that range over arbitrary and possibly higher-order objects in LF [HHP93]. Its most novel features include recursion under λ-binders and matching against dynamically introduced parameters.
This work was sponsored by NSF Grant CCR-9619584 and by the Advanced Research Projects Agency CSTO under the title “The Fox Project: Advanced Languages for Systems Software”, ARPA Order No. C533, issued by ESC/ENS under Contract No. F19628-95-C-0050.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Thierry Coquand. An algorithm for testing conversion in type theory. In Gérard Huet and Gordon Plotkin, editors, Logical Frameworks, pages 255–279. Cambridge University Press, 1991.
Gilles Dowek, Amy Felty, Hugo Herbelin, Gérard Huet, Chet Murthy, Catherine Parent, Christine Paulin-Mohring, and Benjamin Werner. The Coq proof assistant user’s guide. Rapport Techniques 154, INRIA, Roc-quencourt, France, 1993. Version 5.8.
Joëlle Despeyroux, Amy Felty, and André Hirschowitz. Higher-order abstract syntax in Coq. In M. Dezani-Ciancaglini and G. Plotkin, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, pages 124–138, Edinburgh, Scotland, April 1995. Springer-Verlag LNCS 902.
Joelle Despeyroux and Pierre Leleu. Primitive recursion for higher-order abstract syntax with dependent types. In Proceedings of the Workshop on Intuitionistic Modal Logics and Applications (IMPL’99), Trento, Italy, July 1999.
Joëlle Despeyroux, Frank Pfenning, and Carsten Schürmann. Primitive recursion for higher-order abstract syntax. In R. Hindley, editor, Proceedings of the Third International Conference on Typed Lambda Calculus and Applications (TLCA’ 97), pages 147–163, Nancy, France, April 1997. Springer-Verlag LNCS. An extended version is available as Technical Report CMU-CS-96-172, Carnegie Mellon University.
Gerhard Gentzen. Untersuchungen über das logische Schlieβen. Mathematische Zeitschrift, 39:176–210, 405-431, 1935.
Murdoch Gabbay and Andrew Pitts. A new approach to abstract syntax involving binders. In G. Longo, editor, Proceedings of the 14th Annual Symposium on Logic in Computer Science (LICS’99), pages 214–224, Trento, Italy, July 1999. IEEE Computer Society Press.
Lars Hallnäs. A note on the logic of a logic program. In Proceedings of the Workshop on Programming Logic. University of Göteborg and Chalmers University of Technology, Report PMG-R37, 1987.
Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the Association for Computing Machinery, 40(1):143–184, January 1993.
Martin Hofmann. Semantical analysis for higher-order abstract syntax. In G. Longo, editor, Proceedings of the 14th Annual Symposium on Logic in Computer Science (LICS’99), pages 204–213, Trento, Italy, July 1999. IEEE Computer Society Press.
Dale Miller. An extension to ML to handle bound variables in data structures: Preliminary report. In Proceedings of the Logical Frameworks BRA Workshop, Nice, France, May 1990.
Raymond McDowell and Dale Miller. A logic for reasoning with higher-order abstract syntax: An extended abstract. In Glynn Winskel, editor, Proceedings of the Twelfth Annual Symposium on Logic in Computer Science, pages 434–445, Warsaw, Poland, June 1997.
Lawrence C. Paulson. Isabelle: A Generic Theorem Prover. Springer-Verlag LNCS 828, 1994.
Frank Pfenning. Logic programming in the LF logical framework. In Gérard Huet and Gordon Plotkin, editors, Logical Frameworks, pages 149–181. Cambridge University Press, 1991.
Frank Pfenning. Structural cut elimination. In D. Kozen, editor, Proceedings of the Tenth Annual Symposium on Logic in Computer Science, pages 156–166, San Diego, California, June 1995. IEEE Computer Society Press.
Frank Pfenning. Logical frameworks. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning. Elsevier Science Publishers, 1999. In preparation.
A. M. Pitts and M. J. Gabbay. A metalanguage for programming with ound names modulo renaming. In R. Backhouse and J. N. Oliveira, editors, Mathematics of Program Construction, MPC2000, Proceedings, Ponte de Lima, Portugal, July 2000, volume 1837 of Lecture Notes in Computer Science, pages 230–255. Springer-Verlag, Heidelberg, 2000.
Christine Paulin-Mohring. Inductive definitions in the system Coq: Rules and properties. In M. Bezem and J.F. Groote, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, TLCA’93, pages 328–345, Utrecht, The Netherlands, March 1993. Springer-Verlag LNCS 664.
Carsten Schürmann. Automating the Meta-Theory of Deductive Systems. PhD thesis, Carnegie Mellon University, 2000. CMU-CS-00-146.
Peter Schroeder-Heister. Rules of definitional reflection. In M. Vardi, editor, Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science, pages 222–232, Montreal, Canada, June 1993.
Carsten Schürmann and Frank Pfenning. Automated theorem proving in a simple meta-logic for LF. In Claude Kirchner and Hélène Kirchner, editors, Proceedings of the 15th International Conference on Automated Deduction (CADE-15), pages 286–300, Lindau, Germany, July 1998. Springer-Verlag LNCS 1421.
Roberto Virga. Higher-Order Rewriting with Dependent Types. PhD thesis, Department of Mathematical Sciences, Carnegie Mellon University, 1999. Forthcoming.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schürmann, C. (2001). Recursion for Higher-Order Encodings. In: Fribourg, L. (eds) Computer Science Logic. CSL 2001. Lecture Notes in Computer Science, vol 2142. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44802-0_41
Download citation
DOI: https://doi.org/10.1007/3-540-44802-0_41
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42554-0
Online ISBN: 978-3-540-44802-0
eBook Packages: Springer Book Archive