Implicit computation complexity in higher-order programming languages

DOI10.1017/S0960129521000505OpenAlexW4220779078MaRDI QIDQ5875893

Ugo Dal Lago

Publication date: 6 February 2023

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0960129521000505

zbMATH Keywords

computational complexitylinear logiclambda calculustype systems

Mathematics Subject Classification ID

Computer science (68-XX)

Related Items (1)

Read/write factorizable programs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Computation by interaction for space-bounded functional programming
• Bounded combinatory logic and lower complexity
• Realizability models and implicit complexity
• Light logics and optimal reduction: completeness and complexity
• A recursion-theoretic approach to NP
• Functional interpretations of feasibly constructive arithmetic
• \(\lambda\)-definability of free algebras
• Light affine lambda calculus and polynomial time strong normalization
• Lectures on the Curry-Howard isomorphism
• A characterization of lambda definable tree operations
• Soft linear set theory
• A semantic proof of polytime soundness of light affine logic
• Light types for polynomial time computation in lambda calculus
• Quantum implicit computational complexity
• Linear logic by levels and bounded time complexity
• An extension of basic functionality theory for \(\lambda\)-calculus
• Characterizing complexity classes by higher type primitive recursive definitions
• Bounded linear logic: A modular approach to polynomial-time computability
• A new recursion-theoretic characterization of the polytime functions
• Characterizing complexity classes by general recursive definitions in higher types
• Light linear logic
• Ramified recurrence and computational complexity. III: Higher type recurrence and elementary complexity
• Linear types and non-size-increasing polynomial time computation.
• Linear logic and elementary time
• Higher type recursion, ramification and polynomial time
• Safe recursion with higher types and BCK-algebra
• On sharing, memoization, and polynomial time
• An arithmetic for non-size-increasing polynomial-time computation
• Stratified coherence spaces: A denotational semantics for light linear logic
• Realizability models for BLL-like languages
• Soft linear logic and polynomial time
• On an interpretation of safe recursion in light affine logic
• Light affine set theory: A naive set theory of polynomial time
• (Optimal) duplication is not elementary recursive
• On the expressivity of elementary linear logic: characterizing Ptime and an exponential time hierarchy
• An abstract approach to stratification in linear logic
• Linear dependent types in a call-by-value scenario
• The geometry of types
• The geometry of linear higher-order recursion
• Context semantics, linear logic, and computational complexity
• An Implicit Characterization of PSPACE
• On Equivalences, Metrics, and Polynomial Time
• Light logics and higher-order processes
• On session types and polynomial time
• Algebras and coalgebras in the light affine Lambda calculus
• A By-Level Analysis of Multiplicative Exponential Linear Logic
• Linear logic and polynomial time
• Parsimonious Types and Non-uniform Computation
• Characterizing PSPACE with pointers
• Functional Programming in Sublinear Space
• A Soft Type Assignment System for λ-Calculus
• Light Logics and the Call-by-Value Lambda Calculus
• The Computational SLR: A Logic for Reasoning about Computational Indistinguishability
• The Expressiveness of Simple and Second-Order Type Structures
• An Application of Category-Theoretic Semantics to the Characterisation of Complexity Classes Using Higher-Order Function Algebras
• A new “feasible” arithmetic
• Infinitary Lambda Calculi from a Linear Perspective
• FUNCTIONAL PEARL Linear lambda calculus and PTIME-completeness
• Linear Dependent Types and Relative Completeness
• Semantic Evaluation, Intersection Types and Complexity of Simply Typed Lambda Calculus
• Non-uniform Polytime Computation in the Infinitary Affine Lambda-Calculus
• The strength of non-size increasing computation
• Static determination of quantitative resource usage for higher-order programs
• Optimizing optimal reduction
• Polynomial Time in the Parametric Lambda Calculus.
• Foundations of Software Science and Computation Structures
• Computational Complexity
• On the Computational Complexity of Algorithms
• Simple Parsimonious Types and Logarithmic Space
• Multiplexor Categories and Models of Soft Linear Logic
• Verification of Ptime Reducibility for system F Terms: Type Inference in Dual Light Affine Logic
• Programming Languages and Systems
• On light logics, uniform encodings and polynomial time
• Existence and feasibility in arithmetic
• Intuitionistic Light Affine Logic
• Bounded Linear Logic, Revisited
• Theoretical Computer Science
• Computational Complexity

This page was built for publication: Implicit computation complexity in higher-order programming languages