Non-idempotent types for classical calculi in natural deduction style
From MaRDI portal
Publication:5208874
Recommendations
- scientific article; zbMATH DE number 7204443
- A Translation of Intersection and Union Types for the λμ-Calculus
- Complexity of Strongly Normalising λ-Terms via Non-idempotent Intersection Types
- Intersection types for the \(\lambda\mu\)-calculus
- Non-idempotent intersection types and strong normalisation
Cites work
- scientific article; zbMATH DE number 4055576 (Why is no real title available?)
- scientific article; zbMATH DE number 42059 (Why is no real title available?)
- scientific article; zbMATH DE number 1324438 (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 7155170 (Why is no real title available?)
- A Filter Model for the λμ-Calculus
- A Theory of Explicit Substitutions with Safe and Full Composition
- A Translation of Intersection and Union Types for the λμ-Calculus
- A filter lambda model and the completeness of type assignment
- A linearization of the Lambda-calculus and consequences
- A new type assignment for λ-terms
- A nonstandard standardization theorem
- A resource aware computational interpretation for Herbelin's syntax
- A short proof of the strong normalization of classical natural deduction with disjunction
- An estimation for the lengths of reduction sequences of the \(\lambda\mu\rho\theta\)-calculus
- An extension of basic functionality theory for -calculus
- Bounding normalization time through intersection types
- Characterisation of strongly normalising \(\lambda\mu\)-terms
- Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage
- Church-Rosser property of a simple reduction for full first-order classical natural deduction
- Classical by-need
- Classical call-by-need and duality
- Collapsing non-idempotent intersection types
- Complexity of Strongly Normalising λ-Terms via Non-idempotent Intersection Types
- Control categories and duality: On the categorical semantics of the lambda-mu calculus
- Execution time of λ-terms via denotational semantics and intersection types
- Functional Characters of Solvable Terms
- Non-idempotent intersection types and strong normalisation
- Non-idempotent intersection types for the lambda-calculus
- On classical PCF, linear logic and the MIX rule
- Perpetual reductions in -calculus
- Principality and type inference for intersection types using expansion variables
- Proceedings of the sixth workshop on intersection types and related systems, Dubrovnik, Croatia, June 29, 2012
- Quantitative types for the linear substitution calculus
- Reasoning about call-by-need by means of types
- Solvability in resource lambda-calculus
- Sound and complete typing for \(\lambda\mu\)
- The Inhabitation Problem for Non-idempotent Intersection Types
- The duality of computation
- The emptiness problem for intersection types
- The structural \(\lambda \)-calculus
- Typed lambda calculi and applications. 10th international conference, TLCA 2011, Novi Sad, Serbia, June 1--3, 2011. Proceedings
- Types, potency, and idempotency: why nonlinearity and amnesia make a type system work
- Verifying higher-order functional programs with pattern-matching algebraic data types
Cited in
(8)- Tight typings and split bounds, fully developed
- The spirit of node replication
- Quantitative weak linearisation
- A faithful and quantitative notion of distant reduction for the lambda-calculus with generalized applications
- A faithful and quantitative notion of distant reduction for generalized applications
- Node Replication: Theory And Practice
- scientific article; zbMATH DE number 7155170 (Why is no real title available?)
- A subexponential view of domains in session types
This page was built for publication: Non-idempotent types for classical calculi in natural deduction style
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5208874)
