scientific article; zbMATH DE number 7155170
From MaRDI portal
Publication:5208874
Publication date: 22 January 2020
Full work available at URL: https://arxiv.org/abs/1802.05494
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items (6)
Unnamed Item ⋮ Quantitative weak linearisation ⋮ A faithful and quantitative notion of distant reduction for generalized applications ⋮ Node Replication: Theory And Practice ⋮ Tight typings and split bounds, fully developed ⋮ The spirit of node replication
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Typed lambda calculi and applications. 10th international conference, TLCA 2011, Novi Sad, Serbia, June 1--3, 2011. Proceedings
- Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage
- An extension of basic functionality theory for \(\lambda\)-calculus
- Perpetual reductions in \(\lambda\)-calculus
- Church-Rosser property of a simple reduction for full first-order classical natural deduction
- Principality and type inference for intersection types using expansion variables
- Control categories and duality: on the categorical semantics of the lambda-mu calculus
- A Resource Aware Computational Interpretation for Herbelin’s Syntax
- A Translation of Intersection and Union Types for the λμ-Calculus
- Classical By-Need
- Reasoning About Call-by-need by Means of Types
- Non-idempotent intersection types and strong normalisation
- The duality of computation
- Complexity of Strongly Normalising λ-Terms via Non-idempotent Intersection Types
- Classical Call-by-Need and Duality
- A Filter Model for the λμ-Calculus
- Quantitative Types for the Linear Substitution Calculus
- The Inhabitation Problem for Non-idempotent Intersection Types
- A new type assignment for λ-terms
- A filter lambda model and the completeness of type assignment
- A Theory of Explicit Substitutions with Safe and Full Composition
- Solvability in Resource Lambda-Calculus
- The Structural λ-Calculus
- Functional Characters of Solvable Terms
- A linearization of the Lambda-calculus and consequences
- Execution time of λ-terms via denotational semantics and intersection types
- An estimation for the lengths of reduction sequences of the $\lambda\mu\rho\theta$-calculus
- Non-idempotent intersection types for the Lambda-Calculus
- A short proof of the strong normalization of classical natural deduction with disjunction
- The emptiness problem for intersection types
- Types, potency, and idempotency
- A nonstandard standardization theorem
- Verifying higher-order functional programs with pattern-matching algebraic data types
This page was built for publication:
