scientific article; zbMATH DE number 1479634

MaRDI QIDQ4490749zbMATH OpenFDO

Authors Philippa Gardner

Publication date 20 July 2000

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Recommendations

• Needed reduction and spine strategies for the lambda calculus
• Call-by-need, neededness and all that
• Decidable call-by-need computations in term rewriting
• A decidable theory of type assignment
• Reasoning about call-by-need by means of types

Cited in

(33)

• Intersection type assignment systems
• The bang calculus revisited
• The spirit of node replication
• Reasoning about call-by-need by means of types
• A resource aware semantics for a focused intuitionistic calculus
• Inhabitation for non-idempotent intersection types
• Towards a semantic measure of the execution time in call-by-value lambda-calculus
• Sequence types for hereditary permutators
• scientific article; zbMATH DE number 7204443 (Why is no real title available?)
• Tight typings and split bounds, fully developed
• Non-idempotent types for classical calculi in natural deduction style
• Optimizing optimal reduction
• scientific article; zbMATH DE number 7756108 (Why is no real title available?)
• The bang calculus revisited
• Structural rules and algebraic properties of intersection types
• Quantitative weak linearisation
• Node Replication: Theory And Practice
• Minimal relative normalization in orthogonal expression reduction systems
• Characterization of the principal type of normal forms in an intersection type system
• A faithful and quantitative notion of distant reduction for the lambda-calculus with generalized applications
• Categorifying non-idempotent intersection types
• A deep quantitative type system
• A fresh inductive approach to useful call-by-value
• Böhm and Taylor for all!
• Mirroring call-by-need, or values acting silly
• Mechanized subject expansion in uniform intersection types for perpetual reductions
• Meaningfulness and genericity in a subsuming framework (invited talk)
• A quantitative approach to global state composition
• An analysis of symmetry in quantitative semantics
• Hybrid intersection types for PCF
• Mirroring call-by-need, or values acting silly
• Strong normalization through idempotent intersection types: a new syntactical approach
• A correspondence between type checking via reduction and type checking via evaluation

Describes a project that uses

Uses Software

• Miranda

This page was built for publication:

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