A resource aware semantics for a focused intuitionistic calculus
From MaRDI portal
Publication:4559602
DOI10.1017/S0960129517000111zbMath1407.68273OpenAlexW2617563841MaRDI QIDQ4559602
Daniel Lima Ventura, Delia Kesner
Publication date: 4 December 2018
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0960129517000111
Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40)
Related Items
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Linear logic
- The \(\lambda \)-calculus and the unity of structural proof theory
- Theoretical computer science. 8th IFIP TC 1/WG 2.2 international conference, TCS 2014, Rome, Italy, September 1--3, 2014. Proceedings
- The lambda calculus. Its syntax and semantics. Rev. ed.
- An extension of basic functionality theory for \(\lambda\)-calculus
- Complete restrictions of the intersection type discipline
- An equivalence between lambda- terms
- An elementary proof of strong normalization for intersection types
- Principality and type inference for intersection types using expansion variables
- Intersection types for explicit substitutions
- Uniform proofs as a foundation for logic programming
- A Resource Aware Computational Interpretation for Herbelin’s Syntax
- Non-idempotent intersection types and strong normalisation
- Local Bigraphs and Confluence: Two Conjectures
- Complexity of Strongly Normalising λ-Terms via Non-idempotent Intersection Types
- Intersection Types for the Resource Control Lambda Calculi
- 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
- Solvability in Resource Lambda-Calculus
- The Structural λ-Calculus
- Functional Characters of Solvable Terms
- Logic Programming with Focusing Proofs in Linear Logic
- The correspondence between cut-elimination and normalization
- Normalization as a homomorphic image of cut-elimination
- Strong Normalization of Herbelin's Explicit Substitution Calculus with Substitution Propagation
- A semantics for lambda calculi with resources
- Characterising Strongly Normalising Intuitionistic Terms
- 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
