Safety of Nöcker's strictness analysis

DOI10.1017/S0956796807006624MaRDI QIDQ3520168zbMATH OpenFDO

Authors David Sabel, Marko Schütz, Manfred Schmidt-Schauß

Publication date 15 August 2008

Published in Journal of Functional Programming (Search for Journal in Brave)

zbMATH Keywords

contextual semanticsClean compilerfunctional core language

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Functional programming and lambda calculus (68N18)

Recommendations

• On the power and limitations of strictness analysis
• Proving the correctness of compiler optimisations based on a global analysis: a study of strictness analysis^†
• scientific article; zbMATH DE number 3967886
• Publication:4721629
• Strictness and totality analysis

Cites work

• scientific article; zbMATH DE number 675533 (Why is no real title available?)
• scientific article; zbMATH DE number 1952947 (Why is no real title available?)
• scientific article; zbMATH DE number 819768 (Why is no real title available?)
• A co-induction principle for recursively defined domains
• An algebraic interpretation of the K-calculus; and an application of a labelled -calculus
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Deciding inclusion of set constants over infinite non-strict data structures
• Discrimination by parallel observers: the algorithm.
• Lambda calculus with explicit recursion
• Parametric polymorphism and operational equivalence
• Properties of a first-order functional language with sharing
• Secrets of the Glasgow Haskell Compiler inliner
• Skew confluence and the lambda calculus with letrec
• Strictness and totality analysis
• Strictness, totality, and non-standard-type inference
• Term Rewriting and All That
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The revised report on the syntactic theories of sequential control and state

Cited in

(18)

• A Finite Simulation Method in a Non-deterministic Call-by-Need Lambda-Calculus with Letrec, Constructors, and Case
• Similarity implies equivalence in a class of non-deterministic call-by-need lambda calculi
• Nominal unification with letrec and environment-variables
• Counterexamples to applicative simulation and extensionality in non-deterministic call-by-need lambda-calculi with letrec
• Nominal unification with atom-variables
• scientific article; zbMATH DE number 3967886 (Why is no real title available?)
• Proof Tool Support for Explicit Strictness
• Nominal unification with atom and context variables
• Algebraic correctness proofs for compiling recursive function definitions with strictness information
• Contextual Equivalences in Call-by-Need and Call-By-Name Polymorphically Typed Calculi (Preliminary Report)
• Towards Fast Nominal Anti-unification of Letrec-Expressions
• On the power and limitations of strictness analysis
• Making ``stricterness more relevant
• On generic context lemmas for higher-order calculi with sharing
• Deciding inclusion of set constants over infinite non-strict data structures
• scientific article; zbMATH DE number 3995026 (Why is no real title available?)
• Nominal Unification and Matching of Higher Order Expressions with Recursive Let
• scientific article; zbMATH DE number 1617319 (Why is no real title available?)

Describes a project that uses

Uses Software

• Haskell

This page was built for publication: Safety of Nöcker's strictness analysis

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