Selective strictness and parametricity in structural operational semantics, inequationally

DOI10.1016/j.tcs.2007.09.014zbMath1143.68041MaRDI QIDQ2464947

Janis Voigtländer, Patricia Johann

Publication date: 18 December 2007

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: http://libres.uncg.edu/ir/asu/f/Johann_Patricia_Voigtlander_Janis_2007_Selective_Strictness_and_parametricity_.pdf

zbMATH Keywords

seg; types; program transformations; Haskell; lambda calculus; logical relations; parametric polymorphism; functional programming languages; theorems for free; Clean; extensionality principles; fixpoint recursion; identity extension; mixing strict and nonstrict semantics; short cut Fusion

Mathematics Subject Classification ID

68N18: Functional programming and lambda calculus

68Q55: Semantics in the theory of computing

Related Items

A trajectory-based strict semantics for program slicing, A family of syntactic logical relations for the semantics of Haskell-like languages

Uses Software

• Haskell
• GHC

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Functorial polymorphism
• A syntactic theory of sequential control
• A generalization of short-cut fusion and its correctness proof
• A structural approach to operational semantics
• Monadic augment and generalised short cut fusion
• Concatenate, reverse and map vanish for free
• Shortcut fusion for accumulating parameters & zip-like functions
• Secrets of the Glasgow Haskell Compiler inliner
• Free theorems in the presence of seq
• Interpreting Polymorphic FPC into Domain Theoretic Models of Parametric Polymorphism
• Proof Tool Support for Explicit Strictness
• Logical relations and the typed λ-calculus
• Algorithm + strategy = parallelism
• Short cut fusion is correct
• Parametric polymorphism and operational equivalence
• On proving the correctness of program transformations based on free theorems for higher-order polymorphic calculi
• Parametricity of extensionally collapsed term models of polymorphism and their categorical properties
• Mathematics of Program Construction
• Fast and loose reasoning is morally correct
• Boxy types
• The logic of demand in Haskell
• Programming Languages and Systems
• Programming Languages and Systems