A resource aware semantics for a focused intuitionistic calculus

DOI10.1017/S0960129517000111MaRDI QIDQ4559602zbMATH OpenOpenAlexFDO

Authors Delia Kesner, Daniel Lima Ventura

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

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Recommendations

• A resource aware computational interpretation for Herbelin's syntax
• scientific article; zbMATH DE number 7204443
• Structural focalization
• Intersection types for the resource control lambda calculi
• A semantical analysis of focusing and contraction in intuitionistic logic

Cites work

• A filter lambda model and the completeness of type assignment
• A new type assignment for λ-terms
• A nonstandard standardization theorem
• A resource aware computational interpretation for Herbelin's syntax
• A semantics for lambda calculi with resources
• An elementary proof of strong normalization for intersection types
• An equivalence between lambda- terms
• An extension of basic functionality theory for -calculus
• Bounding normalization time through intersection types
• Characterising strongly normalising intuitionistic terms
• Complete restrictions of the intersection type discipline
• Complexity of Strongly Normalising λ-Terms via Non-idempotent Intersection Types
• Functional Characters of Solvable Terms
• scientific article; zbMATH DE number 1670856 (Why is no real title available?)
• scientific article; zbMATH DE number 3735770 (Why is no real title available?)
• scientific article; zbMATH DE number 482822 (Why is no real title available?)
• scientific article; zbMATH DE number 1479634 (Why is no real title available?)
• scientific article; zbMATH DE number 1479641 (Why is no real title available?)
• scientific article; zbMATH DE number 3333259 (Why is no real title available?)
• Intersection types for explicit substitutions
• Intersection types for the resource control lambda calculi
• Linear logic
• Local bigraphs and confluence: two conjectures (extended abstract)
• Logic Programming with Focusing Proofs in Linear Logic
• Non-idempotent intersection types and strong normalisation
• Normalization as a homomorphic image of cut-elimination
• Principality and type inference for intersection types using expansion variables
• Quantitative types for the linear substitution calculus
• Solvability in resource lambda-calculus
• Strong Normalization of Herbelin's Explicit Substitution Calculus with Substitution Propagation
• The \(\lambda \)-calculus and the unity of structural proof theory
• The correspondence between cut-elimination and normalization
• The emptiness problem for intersection types
• The Inhabitation Problem for Non-idempotent Intersection Types
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The structural \(\lambda \)-calculus
• Theoretical computer science. 8th IFIP TC 1/WG 2.2 international conference, TCS 2014, Rome, Italy, September 1--3, 2014. Proceedings
• Types, potency, and idempotency: why nonlinearity and amnesia make a type system work
• Uniform proofs as a foundation for logic programming
• Verifying higher-order functional programs with pattern-matching algebraic data types

Cited in

(5)

• A focus system for the alternation-free \(\mu \)-calculus
• A resource aware computational interpretation for Herbelin's syntax
• A Resource-Aware Semantics and Abstract Machine for a Functional Language with Explicit Deallocation
• Quantitative weak linearisation
• A strong bisimulation for a classical term calculus

This page was built for publication: A resource aware semantics for a focused intuitionistic calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4559602)