More Web Proxy on the site http://driver.im/

Article

Type-Based Productivity of Stream Definitions in the Calculus of Constructions

Author:

Jorge Luis SacchiniAuthors Info & Claims

LICS '13: Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science

Pages 233 - 242

https://doi.org/10.1109/LICS.2013.29

Published: 25 June 2013 Publication History

Abstract

Productivity of core cursive definitions is an essential property in proof assistants since it ensures logical consistency and decidability of type checking. Type-based mechanisms for ensuring productivity use types annotated with size information to track the number of elements produced in core cursive definitions. In this paper, we propose an extension of the Calculus of Constructions-the theory underlying the Coq proof assistant-with a type-based criterion for ensuring productivity of stream definitions. We prove strong normalization and logical consistency. Furthermore, we define an algorithm for inferring size annotations in types. These results can be easily extended to handle general co inductive types.

References

[1]

The Coq Development Team, The Coq Reference Manual, version 8.3, 2009, distributed electronically at http://coq.inria.fr/doc.

[2]

U. Norell, "Towards a practical programming language based on dependent type theory," Ph.D. dissertation, Chalmers University of Technology, 2007.

[3]

F. Blanqui, "A type-based termination criterion for dependently-typed higher-order rewrite systems," in RTA, 2004.

[4]

A. Abel, "A polymorphic lambda-calculus with sized higher-order types," Ph.D. dissertation, Ludwig-Maximilians-Universität München, 2006.

[5]

J. L. Sacchini, "On type-based termination and dependent pattern matching in the Calculus of Inductive Constructions," Ph.D. dissertation, École Nationale Supérieure des Mines de Paris, 2011.

[6]

G. Barthe, B. Grégoire, and F. Pastawski, "CIC: Type-based termination of recursive definitions in the Calculus of Inductive Constructions," in LPAR, 2006.

Digital Library

[7]

B. Grégoire and J. L. Sacchini, "On strong normalization of the calculus of constructions with type-based termination," in LPAR, 2010.

Digital Library

[8]

T. Altenkirch, "Constructions, inductive types and strong normalization," Ph.D. dissertation, University of Edinburgh, Nov. 1993.

[9]

H. Barendregt, "Lambda calculi with types," in Handbook of Logic in Computer Science, 1992.

Digital Library

[10]

G. Barthe, B. Grégoire, and F. Pastawski, "Practical inference for type-based termination in a polymorphic setting," in TLCA, 2005.

Digital Library

[11]

E. Giménez, "A calculus of infinite constructions and its application to the verification of communicating systems," Ph.D. dissertation, Ecole Normale Supérieure de Lyon, 1996.

[12]

C. McBride, "Let's see how things unfold: Reconciling the infinite with the intensional (extended abstract)," in CALCO, 2009.

Digital Library

[13]

A. Abel, B. Pientka, D. Thibodeau, and A. Setzer, "Copatterns: Programming infinite structures by observations," 2013, to appear in POPL'13.

Digital Library

[14]

P.-A. Melliès and B. Werner, "A generic normalisation proof for pure type systems," in TYPES, 1996.

Digital Library

[15]

Z. Luo, Computation and reasoning: a type theory for computer science. Oxford University Press, Inc., 1994.

Digital Library

[16]

B. Werner, "Sets in types, types in sets," in TACS, 1997.

Digital Library

[17]

T. Coquand, "Infinite objects in type theory," in TYPES, 1993.

Digital Library

[18]

N. A. Danielsson and T. Altenkirch, "Subtyping, declaratively," in MPC, 2010.

[19]

A. Abel, "MiniAgda: Integrating sized and dependent types," in PAR, 2010.

[20]

A. Abel, "Type-based termination, inflationary fixed-points, and mixed inductive-coinductive types," in FICS, 2012.

[21]

P. Severi and F.-J. de Vries, "Pure type systems with corecursion on streams: from finite to infinitary normalisation," in ICFP, 2012.

Digital Library

[22]

G. Hutton and M. Jaskelioff, "Representing Contractive Functions on Streams," 2011, submitted to the Journal of Functional Programming.

[23]

K. S. Lars Birkedal, Jan Schwinghammer, "A metric model of lambda calculus with guarded recursion," in FICS, 2010.

[24]

N. R. Krishnaswami and N. Benton, "Ultrametric semantics of reactive programs," in LICS, 2011.

Digital Library

[25]

P. D. Gianantonio and M. Miculan, "A unifying approach to recursive and co-recursive definitions," in TYPES, 2002.

Cited By

Bahr PGraulund CMøgelberg R(2021)Diamonds are not forever: liveness in reactive programming with guarded recursionProceedings of the ACM on Programming Languages10.1145/34342835:POPL(1-28)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434283
Hamza JVoirol NKunčak V(2019)System FR: formalized foundations for the stainless verifierProceedings of the ACM on Programming Languages10.1145/33605923:OOPSLA(1-30)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360592
Lepigre RRaffalli C(2019)Practical Subtyping for Curry-Style LanguagesACM Transactions on Programming Languages and Systems10.1145/328595541:1(1-58)Online publication date: 28-Feb-2019
https://dl.acm.org/doi/10.1145/3285955
Show More Cited By

Index Terms

Type-Based Productivity of Stream Definitions in the Calculus of Constructions

Recommendations

Coinductive Axiomatization of Recursive Type Equality and Subtyping

We present new sound and complete axiomatizations of type equality and subtype inequality for a first-order type language with regular recursive types. The rules are motivated by coinductive characterizations of type containment and type equality via ...
Typed closure conversion for the calculus of constructions
PLDI 2018: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation

Dependently typed languages such as Coq are used to specify and verify the full functional correctness of source programs. Type-preserving compilation can be used to preserve these specifications and proofs of correctness through compilation into the ...
Characterization of strong normalizability for a sequent lambda calculus with co-control
PPDP '17: Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming

We study strong normalization in a lambda calculus of proof-terms with co-control for the intuitionistic sequent calculus. In this sequent lambda calculus, the management of formulas on the left hand side of typing judgements is "dual" to the management ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

LICS '13: Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science

June 2013

597 pages

ISBN:9780769550206

Sponsors

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

IEEE Computer Society

United States

Publication History

Published: 25 June 2013

Check for updates

Author Tags

Qualifiers

Article

Acceptance Rates

Overall Acceptance Rate 215 of 622 submissions, 35%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
34
Total Downloads

Downloads (Last 12 months)1
Downloads (Last 6 weeks)0

Reflects downloads up to 21 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Bahr PGraulund CMøgelberg R(2021)Diamonds are not forever: liveness in reactive programming with guarded recursionProceedings of the ACM on Programming Languages10.1145/34342835:POPL(1-28)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434283
Hamza JVoirol NKunčak V(2019)System FR: formalized foundations for the stainless verifierProceedings of the ACM on Programming Languages10.1145/33605923:OOPSLA(1-30)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360592
Lepigre RRaffalli C(2019)Practical Subtyping for Curry-Style LanguagesACM Transactions on Programming Languages and Systems10.1145/328595541:1(1-58)Online publication date: 28-Feb-2019
https://dl.acm.org/doi/10.1145/3285955
Danielsson N(2017)Up-to techniques using sized typesProceedings of the ACM on Programming Languages10.1145/31581312:POPL(1-28)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158131
Abel AÖhman JVezzosi A(2017)Decidability of conversion for type theory in type theoryProceedings of the ACM on Programming Languages10.1145/31581112:POPL(1-29)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158111
Abel AVezzosi AWinterhalter T(2017)Normalization by evaluation for sized dependent typesProceedings of the ACM on Programming Languages10.1145/31102771:ICFP(1-30)Online publication date: 29-Aug-2017
https://dl.acm.org/doi/10.1145/3110277
Severi P(2017)A Light Modality for RecursionProceedings of the 20th International Conference on Foundations of Software Science and Computation Structures - Volume 1020310.1007/978-3-662-54458-7_29(499-516)Online publication date: 22-Apr-2017
https://dl.acm.org/doi/10.1007/978-3-662-54458-7_29
Basold HGeuvers HKoskinen EGrohe MShankar N(2016)Type Theory based on Dependent Inductive and Coinductive TypesProceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/2933575.2934514(327-336)Online publication date: 5-Jul-2016
https://dl.acm.org/doi/10.1145/2933575.2934514
Møgelberg RHenzinger TMiller D(2014)A type theory for productive coprogramming via guarded recursionProceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1145/2603088.2603132(1-10)Online publication date: 14-Jul-2014
https://dl.acm.org/doi/10.1145/2603088.2603132

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents