Linear Dependent Types and Relative Completeness

Ugo Dal Lago; Marco Gaboardi

doi:10.2168/LMCS-8(4:11)2012

Ugo Dal Lago ; Marco Gaboardi - Linear Dependent Types and Relative Completeness

lmcs:974 - Logical Methods in Computer Science, October 23, 2012, Volume 8, Issue 4 - https://doi.org/10.2168/LMCS-8(4:11)2012

Linear Dependent Types and Relative CompletenessArticle

Authors: Ugo Dal Lago ; Marco Gaboardi

A system of linear dependent types for the lambda calculus with full higher-order recursion, called dlPCF, is introduced and proved sound and relatively complete. Completeness holds in a strong sense: dlPCF is not only able to precisely capture the functional behaviour of PCF programs (i.e. how the output relates to the input) but also some of their intensional properties, namely the complexity of evaluating them with Krivine's Machine. dlPCF is designed around dependent types and linear logic and is parametrized on the underlying language of index terms, which can be tuned so as to sacrifice completeness for tractability.

https://doi.org/10.2168/LMCS-8(4:11)2012

Source: arXiv.org:1104.0193

Volume: Volume 8, Issue 4

Published on: October 23, 2012

Imported on: December 29, 2011

Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages,F.3.2, F.3.1

Licence: arXiv.org - Non-exclusive license to distribute

Funding:

Source : OpenAIRE Graph

PRACTICAL LIGHT TYPES FOR RESOURCE CONSUMPTION; Funder: European Commission; Code: 272487

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

14 Documents citing this article

Claudia Faggian;Daniele Pautasso;Gabriele Vanoni, 2024, Higher Order Bayesian Networks, Exactly, Proceedings of the ACM on Programming Languages, 8, POPL, pp. 2514-2546, 10.1145/3632926, https://doi.org/10.1145/3632926.

Ugo Dal Lago;Claudia Faggian;Simona Ronchi Della Rocca, 2021, Intersection types and (positive) almost-sure termination, Proceedings of the ACM on Programming Languages, 5, POPL, pp. 1-32, 10.1145/3434313, https://doi.org/10.1145/3434313.

Vineet Rajani;Marco Gaboardi;Deepak Garg;Jan Hoffmann, 2021, A unifying type-theory for higher-order (amortized) cost analysis, Proceedings of the ACM on Programming Languages, 5, POPL, pp. 1-28, 10.1145/3434308, https://doi.org/10.1145/3434308.

Patrick Baillot;Gilles Barthe;Ugo Dal Lago, 2019, Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs, 63, 4, pp. 813-855, 10.1007/s10817-019-09530-2, https://hal.archives-ouvertes.fr/hal-02399471.

Ugo Dal Lago;Marc de Visme;Damiano Mazza;Akira Yoshimizu, 2019, Intersection types and runtime errors in the pi-calculus, Proceedings of the ACM on Programming Languages, 3, POPL, pp. 1-29, 10.1145/3290320, https://doi.org/10.1145/3290320.

Martin Avanzini;Ugo Dal Lago, 2017, Automated Sized-Type Inference and Complexity Analysis, arXiv (Cornell University), 248, pp. 7-16, 10.4204/eptcs.248.5.

Van Chan Ngo;Mario Dehesa-Azuara;Matthew Fredrikson;Jan Hoffmann, arXiv (Cornell University), Verifying and Synthesizing Constant-Resource Implementations with Types, pp. 710-728, 2017, San Jose, CA, 10.1109/sp.2017.53, https://arxiv.org/abs/1801.01896.

Soichiro Fujii;Shin-ya Katsumata;Paul-André Melliès, Lecture notes in computer science, Towards a Formal Theory of Graded Monads, pp. 513-530, 2016, 10.1007/978-3-662-49630-5_30.

Aloïs Brunel;Marco Gaboardi, 2015, Realizability models for a linear dependent PCF, Theoretical Computer Science, 585, pp. 55-70, 10.1016/j.tcs.2015.03.005, https://doi.org/10.1016/j.tcs.2015.03.005.

Martin Avanzini;Ugo Dal Lago;Georg Moser, 2015, Analysing the complexity of functional programs: higher-order meets first-order, ACM SIGPLAN Notices, 50, 9, pp. 152-164, 10.1145/2858949.2784753, https://hal.inria.fr/hal-01231809.

Martin Avanzini;Ugo Dal Lago;Georg Moser, Analysing the complexity of functional programs: higher-order meets first-order, 2015, Vancouver BC Canada, 10.1145/2784731.2784753, https://hal.inria.fr/hal-01231809.

Dan R. Ghica;Alex I. Smith, Lecture notes in computer science, Bounded Linear Types in a Resource Semiring, pp. 331-350, 2014, 10.1007/978-3-642-54833-8_18, https://doi.org/10.1007/978-3-642-54833-8_18.

Damiano Mazza, Lecture notes in computer science, Non-linearity as the Metric Completion of Linearity, pp. 3-14, 2013, 10.1007/978-3-642-38946-7_3.

Ugo Dal Lago;Giulio Pellitta, Complexity Analysis in Presence of Control Operators and Higher-Order Functions, pp. 258-273, 2013, 10.1007/978-3-642-45221-5_19, https://hal.inria.fr/hal-00909319.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 1885 times.

This article's PDF has been downloaded 432 times.