A Calculus of Inductive Linear Constructions
Authors: 
Qiancheng Fu, Hongwei XiAuthors Info & Claims
Pages 1 - 13
Abstract
In this paper, we present a novel calculus of inductive linear constructions (CILC), combining linear types and dependent types. Our type theory addresses a looming issue in the research on linear dependent types: the lack of a general mechanism for defining sound linear inductive types. CILC allows one to encode in a straightforward manner the linear connectives that must be baked into the core of other systems. This greatly lowers the difficulty of encoding various data structures and makes writing non-trivial programs humanly feasible. We study the standard meta theory of our calculus, showing that it is sound in the usual sense. Through a heap-based operational semantics, we show that CILC safely manipulates resources and runs memory clean. We have formalized and proven correct most of the reported results in the Coq Proof Assistant.
References
[1]
Samson Abramsky. 1993. Computational interpretations of linear logic. Theoretical Computer Science, 111, 1 (1993), 3–57. issn:0304-3975 https://doi.org/10.1016/0304-3975(93)90181-R
[2]
Robert Atkey. 2018. The Syntax and Semantics of Quantitative Type Theory. In LICS ’18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, July 9–12, 2018, Oxford, United Kingdom. https://doi.org/10.1145/3209108.3209189
[3]
Andrew G. Barber and Gordan Plotkin. 1996. Dual Intuitionistic Linear Logic. Labrartory of Compute Science, Univerity of Edinburgh.
[4]
Bruno Barras. 2012. Semantical Investigations in Intuitionistic Set Theory and Type Theories with Inductive Families.
[5]
P. N. Benton. 1995. A mixed linear and non-linear logic: Proofs, terms and models. In Computer Science Logic, Leszek Pacholski and Jerzy Tiuryn (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 121–135. isbn:978-3-540-49404-1
[6]
Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, and Arnaud Spiwack. 2017. Linear Haskell: Practical Linearity in a Higher-Order Polymorphic Language. Proc. ACM Program. Lang., 2, POPL (2017), Article 5, dec, 29 pages. https://doi.org/10.1145/3158093
[7]
Iliano Cervesato and Frank Pfenning. 2002. A Linear Logical Framework. Information and Computation, 179, 1 (2002), 19–75. issn:0890-5401 https://doi.org/10.1006/inco.2001.2951
[8]
Pritam Choudhury, Harley Eades III, Richard A. Eisenberg, and Stephanie Weirich. 2021. A Graded Dependent Type System with a Usage-Aware Semantics. Proc. ACM Program. Lang., 5, POPL (2021), Article 50, jan, 32 pages. https://doi.org/10.1145/3434331
[9]
Thierry Coquand and Christine Paulin. 1988. Inductively defined types. In COLOG-88, International Conference on Computer Logic, Tallinn, USSR, December 1988, Proceedings, Per Martin-Löf and Grigori Mints (Eds.) (Lecture Notes in Computer Science, Vol. 417). Springer, 50–66. https://doi.org/10.1007/3-540-52335-9_47
[10]
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. The Lean Theorem Prover (System Description). In Automated Deduction - CADE-25, Amy P. Felty and Aart Middeldorp (Eds.). Springer International Publishing, Cham. 378–388. isbn:978-3-319-21401-6
[11]
Peter Dybjer. 1997. Inductive Families. Formal Aspects of Computing, 6 (1997), 440–465.
[12]
Qiancheng Fu and Hongwei Xi. 2023. Formalization and Implementation of CILC. https://doi.org/10.1145/3580404
[13]
Jean-Yves Girard. 1987. Linear logic. Theoretical Computer Science, 50, 1 (1987), 1–101. issn:0304-3975 https://doi.org/10.1016/0304-3975(87)90045-4
[14]
Robert Harper, Furio Honsell, and Gordon Plotkin. 1993. A Framework for Defining Logics. J. ACM, 40, 1 (1993), Jan., 143–184. issn:0004-5411 https://doi.org/10.1145/138027.138060
[15]
Neelakantan R. Krishnaswami, Pierre Pradic, and Nick Benton. 2015. Integrating Linear and Dependent Types. SIGPLAN Not., 50, 1 (2015), Jan., 17–30. issn:0362-1340 https://doi.org/10.1145/2775051.2676969
[16]
Per Martin-Löf. 1984. Intuitionistic type theory (Studies in proof theory, Vol. 1). Bibliopolis. isbn:978-88-7088-228-5
[17]
Conor McBride. 2000. Elimination with a Motive. In Types for Proofs and Programs, International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000, Selected Papers, Paul Callaghan, Zhaohui Luo, James McKinna, and Robert Pollack (Eds.) (Lecture Notes in Computer Science, Vol. 2277). Springer, 197–216. https://doi.org/10.1007/3-540-45842-5_13
[18]
Conor McBride. 2016. I Got Plenty o’ Nuttin’. In A List of Successes That Can Change the World.
[19]
Ulf Norell. 2007. Towards a practical programming language based on dependent type theory.
[20]
Christine Paulin-Mohring. 1993. Inductive definitions in the system Coq rules and properties. In Typed Lambda Calculi and Applications, Marc Bezem and Jan Friso Groote (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 328–345. isbn:978-3-540-47586-6
[21]
M. Takahashi. 1995. Parallel Reductions in λ -Calculus. Inf. Comput., 118, 1 (1995), April, 120–127. issn:0890-5401 https://doi.org/10.1006/inco.1995.1057
[22]
The Coq Development Team. 2020. The Coq Proof Assistant, version 8.11.0. https://doi.org/10.5281/ZENODO.3744225
[23]
The Rust teams. 2022. Rust Programming Language. http://www.rust-lang.org/
[24]
Jesse A. Tov and Riccardo Pucella. 2011. Practical Affine Types. SIGPLAN Not., 46, 1 (2011), jan, 447–458. issn:0362-1340 https://doi.org/10.1145/1925844.1926436
[25]
David N. Turner and Philip Wadler. 1999. Operational interpretations of linear logic. Theoretical Computer Science, 227, 1 (1999), 231–248. issn:0304-3975 https://doi.org/10.1016/S0304-3975(99)00054-7
[26]
Matthijs Vákár. 2014. Syntax and Semantics of Linear Dependent Types. CoRR, abs/1405.0033 (2014), arXiv:1405.0033. arxiv:1405.0033
[27]
P. Wadler. 1990. Linear Types can Change the World!. In Programming Concepts and Methods.
[28]
P. Wadler. 1991. There’s No Substitute for Linear Logic.
[29]
Hongwei Xi. 2007. Dependent ML An approach to practical programming with dependent types. Journal of Functional Programming, 17, 2 (2007), 215–286. https://doi.org/10.1017/S0956796806006216
[30]
Hongwei Xi. 2010. The ATS Programming Language. http://www.ats-lang.org/
Index Terms
- A Calculus of Inductive Linear Constructions
Index terms have been assigned to the content through auto-classification.
Recommendations
Type Theory based on Dependent Inductive and Coinductive Types
LICS '16: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer ScienceWe develop a dependent type theory that is based purely on inductive and coinductive types, and the corresponding recursion and corecursion principles. This results in a type theory with a small set of rules, while still being fairly expressive. For ...
Integrating Linear and Dependent Types
POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesIn this paper, we show how to integrate linear types with type dependency, by extending the linear/non-linear calculus of Benton to support type dependency. Next, we give an application of this calculus by giving a proof-theoretic account of imperative ...
Inductive types deconstructed: the calculus of united constructions
TyDe 2019: Proceedings of the 4th ACM SIGPLAN International Workshop on Type-Driven DevelopmentAlgebraic data types and inductive types like those of the Calculus of Inductive Constructions (CIC) are the bread and butter of statically typed functional programming languages. They conveniently combine in a single package product types, sum types, ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
August 2023
70 pages
Copyright © 2023 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 31 August 2023
Check for updates
Badges
Author Tags
Qualifiers
- Research-article
Conference
TyDe '23
Sponsor:
TyDe '23: 8th ACM SIGPLAN International Workshop on Type-Driven Development
September 4, 2023
WA, Seattle, USA
Upcoming Conference
ICFP '25
- Sponsor:
- sigplan
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 108Total Downloads
- Downloads (Last 12 months)49
- Downloads (Last 6 weeks)7
Reflects downloads up to 10 Nov 2024
Other Metrics
Citations
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in