Cover Image

Simply typed convertibility is TOWER-complete even for safe lambda-terms

Fuente: arXiv

Saved in:

Bibliographic Details
Main Author:	Nguyên, Lê Thành Dũng
Format:	Preprint
Published:	2023
Subjects:	Logic in Computer Science Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Syntactically and semantically regular languages of lambda-terms coincide through logical relations
by: Moreau, Vincent, et al.
Published: (2023)

On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus
by: Kobayashi, Naoki
Published: (2024)

Function spaces for orbit-finite sets
by: Bojańczyk, Mikołaj, et al.
Published: (2024)

Slightly Non-Linear Higher-Order Tree Transducers
by: Nguyên, Lê Thành Dũng, et al.
Published: (2024)

Uniform Algebras: Models and constructive Completeness for Full, Simply Typed λProlog
by: Amato, Gianluca, et al.
Published: (2024)

The structure of polynomial growth for tree automata/transducers and MSO set queries
by: Gallot, Paul, et al.
Published: (2025)

Tree transducers of linear size-to-height increase (and the additive conjunction of linear logic)
by: Dartois, Luc, et al.
Published: (2026)

An extended type system with lambda-typed lambda-expressions (extended version)
by: Weber, Matthias
Published: (2018)

Profinite lambda-terms and parametricity
by: van Gool, Sam, et al.
Published: (2023)

A System of Interaction and Structure III: The Complexity of BV and Pomset Logic
by: Nguyên, Lê Thành Dũng, et al.
Published: (2022)

Multi types and reasonable space
by: Accattoli, Beniamino, et al.
Published: (2022)

Compositional Verification in Concurrent Separation Logic with Permissions Regions
by: Le, Quang Loc
Published: (2025)

A formalization of System I with type Top in Agda
by: Séttimo, Agustín, et al.
Published: (2026)

Cyclic Proofs in Hoare Logic and its Reverse
by: Brotherston, James, et al.
Published: (2025)

A concrete model for a typed linear algebraic lambda calculus
by: Díaz-Caro, Alejandro, et al.
Published: (2018)

Frex: dependently-typed algebraic simplification
by: Allais, Guillaume, et al.
Published: (2023)

Kleene algebra with commutativity conditions is undecidable
by: de Amorim, Arthur Azevedo, et al.
Published: (2024)

On the complexity of normalization for the planar $λ$-calculus
by: Das, Anupam, et al.
Published: (2024)

Foundations of Digital Circuits: Denotation, Operational, and Algebraic Semantics
by: Kaye, George
Published: (2025)

Impredicativity in Linear Dependent Type Theory
by: Speight, Sam, et al.
Published: (2026)

Crash-Stop Failures in Asynchronous Multiparty Session Types
by: Barwell, Adam D., et al.
Published: (2023)

On Complexity Bounds and Confluence of Parallel Term Rewriting
by: Baudon, Thaïs, et al.
Published: (2023)

Types, equations, dimensions and the Pi theorem
by: Botta, Nicola, et al.
Published: (2023)

A flexible specification approach for verifying total correctness of fine-grained concurrent modules
by: Fasse, Justus, et al.
Published: (2023)

An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification
by: Elad, Neta, et al.
Published: (2023)

Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects
by: Zilberstein, Noam, et al.
Published: (2023)

Higher-Order Asynchronous Effects
by: Ahman, Danel, et al.
Published: (2023)

Rely-Guarantee Reasoning for Causally Consistent Shared Memory (Extended Version)
by: Lahav, Ori, et al.
Published: (2023)

A Saturation-Based Unification Algorithm for Higher-Order Rational Patterns
by: Chen, Zhibo, et al.
Published: (2023)

A denotationally-based program logic for higher-order store
by: Aagaard, Frederik Lerbjerg, et al.
Published: (2023)

Structural Analysis of GRAFCET Control Specifications
by: Schnakenbeck, Aron, et al.
Published: (2023)

A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests
by: Kappé, Tobias, et al.
Published: (2023)

A feasible and unitary quantum programming language
by: Díaz-Caro, Alejandro, et al.
Published: (2023)

Proving Confluence in the Confluence Framework with CONFident
by: Gutiérrez, Raúl, et al.
Published: (2023)

Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions
by: Klinkenberg, Lutz, et al.
Published: (2023)

Checkpoint-based rollback recovery in session programming
by: Mezzina, Claudio Antares, et al.
Published: (2023)

Layered Modal Type Theories
by: Hu, Jason Z. S., et al.
Published: (2023)

Typed compositional quantum computation with lenses
by: Garrigue, Jacques, et al.
Published: (2023)

Dependent Type Refinements for Futures
by: Somayyajula, Siva, et al.
Published: (2023)

Extending Isabelle/HOL's Code Generator with support for the Go programming language
by: Stübinger, Terru, et al.
Published: (2023)