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.

Comment: 44 pages, 1 figure

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

Source: arXiv.org:1104.0193

Volume: Volume 8, Issue 4

Secondary volumes: Selected Papers of the 26th IEEE Symposium on Logic in Computer Science (LICS 2011)

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, Electronic Proceedings in Theoretical Computer Science, 248, pp. 7-16, 10.4204/eptcs.248.5, https://doi.org/10.4204/eptcs.248.5.

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

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

Aloïs Brunel;Marco Gaboardi, 2015, Realizability models for a linear dependent PCF, Discovery Research Portal (University of Dundee), 585, pp. 55-70, 10.1016/j.tcs.2015.03.005, https://discovery.dundee.ac.uk/en/publications/057ae60f-91ae-4456-944a-8567cf5129c9.

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.

Martin Avanzini;Ugo Dal Lago;Georg Moser, 2015, Analysing the complexity of functional programs: higher-order meets first-order, SPIRE - Sciences Po Institutional REpository, pp. 152-164, 10.1145/2784731.2784753, https://inria.hal.science/hal-01231809.

Dan R. Ghica;Alex I. Smith, 2014, Bounded Linear Types in a Resource Semiring, University of Birmingham Research Portal (University of Birmingham), pp. 331-350, 10.1007/978-3-642-54833-8_18, http://www.scopus.com/inward/record.url?scp=84900522404&partnerID=8YFLogxK.

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

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

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 3522 times.

This article's PDF has been downloaded 680 times.