Document Open Access Logo

Well-Founded Recursion over Contextual Objects

Authors Brigitte Pientka, Andreas Abel

PDF

File

Thumbnail PDF
PDF
LIPIcs.TLCA.2015.273.pdf
  • Filesize: 0.52 MB
  • 15 pages

Document Identifiers

Subject Classification

Keywords
  • Type systems
  • Dependent Types
  • Logical Frameworks

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We present a core programming language that supports writing well-founded structurally recursive functions using simultaneous pattern matching on contextual LF objects and contexts. The main technical tool is a coverage checking algorithm that also generates valid recursive calls. To establish consistency, we define a call-by-value small-step semantics and prove that every well-typed program terminates using a reducibility semantics. Based on the presented methodology we have implemented a totality checker as part of the programming and proof environment Beluga where it can be used to establish that a total Beluga program corresponds to a proof.

Cite As Get BibTex

Brigitte Pientka and Andreas Abel. Well-Founded Recursion over Contextual Objects. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 273-287, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.TLCA.2015.273

Author Details

Brigitte Pientka
Andreas Abel

References

  1. Andreas Abel. Tutch User’s Guide. Carnegie-Mellon University, Pittsburgh, PA, 2002. Section 7.1: Proof terms for structural recursion. Google Scholar
  2. Andreas Abel and Brigitte Pientka. Higher-order dynamic pattern unification for dependent types and records. In TLCA'11, volume 6690 of LNCS, pages 10-26. Springer, 2011. Google Scholar
  3. Olivier Savary Belanger, Stefan Monnier, and Brigitte Pientka. Programming type-safe transformations using higher-order abstract syntax. In CPP'13, volume 8307 of LNCS, pages 243-258. Springer, 2013. Google Scholar
  4. Andrew Cave and Brigitte Pientka. Programming with binders and indexed data-types. In POPL'12, pages 413-424. ACM, 2012. Google Scholar
  5. Joshua Dunfield and Brigitte Pientka. Case analysis of higher-order data. ENTCS, 228:69-84, 2009. Google Scholar
  6. Francisco Ferreira and Brigitte Pientka. Bidirectional elaboration of dependently typed languages. In PPDP'14. ACM, 2014. Google Scholar
  7. Andrew Gacek, Dale Miller, and Gopalan Nadathur. Combining generic judgments with recursive definitions. In LICS'08, pages 33-44. IEEE CS Press, 2008. Google Scholar
  8. Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. JACM, 40(1):143-184, 1993. Google Scholar
  9. Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. Contextual modal type theory. ACM TOCL, 9(3):1-49, 2008. Google Scholar
  10. Brigitte Pientka. Verifying termination and reduction properties about higher-order logic programs. JAR, 34(2):179-207, 2005. Google Scholar
  11. Brigitte Pientka. A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In POPL'08, pages 371-382. ACM, 2008. Google Scholar
  12. Brigitte Pientka. An insider’s look at LF type reconstruction: Everything you (n)ever wanted to know. JFP, 1(1-37), 2013. Google Scholar
  13. Brigitte Pientka and Joshua Dunfield. Beluga: A framework for programming and reasoning with deductive systems (system description). In IJCAR'10, volume 6173 of LNCS, pages 15-21. Springer, 2010. Google Scholar
  14. Andrew Pitts. Nominal logic, a first order theory of names and binding. Inf. Comput., 186(2):165-193, 2003. Google Scholar
  15. Carsten Schürmann. Automating the Meta Theory of Deductive Systems. PhD thesis, Department of Computer Science, Carnegie Mellon University, 2000. CMU-CS-00-146. Google Scholar
  16. Carsten Schürmann, Joëlle Despeyroux, and Frank Pfenning. Primitive recursion for higher-order abstract syntax. TCS, 266(1-2):1-57, 2001. Google Scholar
  17. Carsten Schürmann and Frank Pfenning. A coverage checking algorithm for LF. In TPHOLS'03, volume 2758 of LNCS, pages 120-135, Rome, Italy, 2003. Springer. Google Scholar
  18. Alwen Tiu and Alberto Momigliano. Cut elimination for a logic with induction and co-induction. J. Applied Logic, 10(4):330-367, 2012. Google Scholar
  19. Roberto Virga. Higher-Order Rewriting with Dependent Types. PhD thesis, Department of Mathematical Sciences, Carnegie Mellon University, 1999. CMU-CS-99-167. Google Scholar
  20. Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. A concurrent logical framework I: Judgements and properties. Technical report, School of Computer Science, Carnegie Mellon University, Pittsburgh, 2003. Google Scholar
  21. Hongwei Xi. Dependent types for program termination verification. HOSC, 15(1):91-131, 2002. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact