Document Open Access Logo

Index-Stratified Types

Authors Rohan Jacob-Rao, Brigitte Pientka, David Thibodeau

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2018.19.pdf
  • Filesize: 0.56 MB
  • 17 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Logic and verification
Keywords
  • Indexed types
  • (co)recursive types
  • logical relations

Metrics

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

Abstract

We present Tores, a core language for encoding metatheoretic proofs. The novel features we introduce are well-founded Mendler-style (co)recursion over indexed data types and a form of recursion over objects in the index language to build new types. The latter, which we call index-stratified types, are analogue to the concept of large elimination in dependently typed languages. These features combined allow us to encode sophisticated case studies such as normalization for lambda calculi and normalization by evaluation. We prove the soundness of Tores as a programming and proof language via the key theorems of subject reduction and termination.

Cite As Get BibTex

Rohan Jacob-Rao, Brigitte Pientka, and David Thibodeau. Index-Stratified Types. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 19:1-19:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.FSCD.2018.19

Author Details

Rohan Jacob-Rao
  • Digital Asset, Sydney, Australia
Brigitte Pientka
  • McGill University, Montreal, Canada
David Thibodeau
  • McGill University, Montreal, Canada

Funding

This research was funded by the Natural Science and Engineering Research Council Canada (NSERC).

References

  1. Andreas Abel and Ralph Matthes. Fixed points of type constructors and primitive recursion. In 18th Int'l Workshop on Computer Science Logic (CSL'04), Lecture Notes in Computer Science (LNCS 3210), pages 190-204. Springer, 2004. Google Scholar
  2. Ki Yung Ahn. The Nax Language: Unifying Functional Programming and Logical Reasoning in a Language based on Mendler-style Recursion Schemes and Term-indexed Types. PhD thesis, Portland State University, 2014. Google Scholar
  3. David Baelde and Gopalan Nadathur. Combining deduction modulo and logics of fixed-point definitions. In 27th Annual IEEE Symp. on Logic in Computer Science (LICS'12), pages 105-114. IEEE, 2012. Google Scholar
  4. Andrew Cave and Brigitte Pientka. Programming with binders and indexed data-types. In 39th ACM Symp. on Principles of Programming Languages (POPL'12), pages 413-424. ACM, 2012. Google Scholar
  5. Andrew Cave and Brigitte Pientka. First-class substitutions in contextual type theory. In 8th ACM Int'l Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'13), pages 15-24. ACM, 2013. Google Scholar
  6. Andrew Cave and Brigitte Pientka. A case study on logical relations using contextual types. In 10th Int'l Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'15), pages 18-33. Electronic Proceedings in Theoretical Computer Science (EPTCS), 2015. Google Scholar
  7. James Cheney and Ralf Hinze. First-class phantom types. Technical Report CUCIS TR2003-1901, Cornell University, 2003. Google Scholar
  8. Gilles Dowek, Thérèse Hardin, and Claude Kirchner. Theorem proving modulo. Journal of Automated Reasoning, 31(1):33-72, 2003. Google Scholar
  9. Gilles Dowek and Benjamin Werner. Proof normalization modulo. J. Symb. Log., 68(4):1289-1316, 2003. Google Scholar
  10. J. Y Girard. Interprétation fonctionnelle et elimination des coupures de l'arithmétique d'ordre supérieur. These d'état, Université de Paris 7, 1972. Google Scholar
  11. Rohan Jacob-Rao, Andrew Cave, and Brigitte Pientka. Mechanizing proofs about Mendler-style recursion. In 11th Int'l Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'16), pages 1-9. ACM, 2016. Google Scholar
  12. Raymond C. McDowell and Dale A. Miller. Reasoning with higher-order abstract syntax in a logical framework. ACM Transactions on Computational Logic, 3(1):80-136, 2002. Google Scholar
  13. Nax Paul Francis Mendler. Inductive Definition in Type Theory. PhD thesis, Cornell University, Ithaca, NY, USA, 1988. AAI8804634. Google Scholar
  14. Alberto Momigliano and Alwen Fernanto Tiu. Induction and co-induction in sequent calculus. In Types for Proofs and Programs (TYPES'03), Lecture Notes in Computer Science (LNCS 3085), pages 293-308. Springer, 2004. Google Scholar
  15. Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. Contextual modal type theory. ACM Transactions on Computational Logic, 9(3):1-49, 2008. Google Scholar
  16. Brigitte Pientka. A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In 35th ACM Symp. on Principles of Programming Languages (POPL'08), pages 371-382. ACM, 2008. Google Scholar
  17. Brigitte Pientka and Andreas Abel. Structural recursion over contextual objects. In 13th Int'l Conf. on Typed Lambda Calculi and Applications (TLCA'15), pages 273-287. Leibniz Int'l Proceedings in Informatics (LIPIcs) of Schloss Dagstuhl, 2015. Google Scholar
  18. Brigitte Pientka and Joshua Dunfield. Programming with proofs and explicit contexts. In 35th ACM Symp. on Principles and Practice of Declarative Programming (PPDP'08), pages 163-173. ACM, 2008. Google Scholar
  19. Peter Schroeder-Heister. Rules of definitional reflection. In 8th Annual Symp. on Logic in Computer Science (LICS '93), pages 222-232. IEEE Computer Society, 1993. Google Scholar
  20. William Tait. Intensional Interpretations of Functionals of Finite Type I. J. Symb. Log., 32(2):198-212, 1967. Google Scholar
  21. David Thibodeau, Andrew Cave, and Brigitte Pientka. Indexed codata. In 21st ACM Int'l Conf. on Functional Programming (ICFP'16), pages 351-363. ACM, 2016. Google Scholar
  22. Alwen Tiu. Stratification in logics of definitions. In 6th Int'l Joint Conf. on Automated Reasoning (IJCAR'12), Lecture Notes in Computer Science (LNCS 7364), pages 544-558. Springer, 2012. Google Scholar
  23. 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
  24. Hongwei Xi, Chiyan Chen, and Gang Chen. Guarded recursive datatype constructors. In 30th ACM Symp. on Principles of Programming Languages (POPL'03), pages 224-235. ACM, 2003. 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