Type systems equivalent to data-flow analyses for imperative languages

DOI10.1016/J.TCS.2006.08.013MaRDI QIDQ860844zbMATH OpenOpenAlexWikidataFDO

Authors Peeter Laud, Tarmo Uustalu, Varmo Vene

Publication date 9 January 2007

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

Full work available at URL https://doi.org/10.1016/j.tcs.2006.08.013

zbMATH Keywords

type systemssecure information flowdata-flow analyses

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Recommendations

• Substructural Type Systems for Program Analysis
• Bidirectional data flow analysis for type inferencing.
• Type-based flow analysis and context-free language reachability
• Type inference for pure type systems
• scientific article; zbMATH DE number 2087535
• scientific article; zbMATH DE number 1130261

Cites work

• scientific article; zbMATH DE number 1692935 (Why is no real title available?)
• scientific article; zbMATH DE number 1324833 (Why is no real title available?)
• scientific article; zbMATH DE number 1956552 (Why is no real title available?)
• scientific article; zbMATH DE number 1538021 (Why is no real title available?)
• An Axiomatic Approach to Information Flow in Programs
• Certification of programs for secure information flow
• Cryptography. Theory and practice
• From polyvariant flow information to intersection and union types
• Lightweight bytecode verification
• Logic for Programming, Artificial Intelligence, and Reasoning
• On flow-sensitive security types
• Oracle-based checking of untrusted software
• Programming Languages and Systems
• Static Analysis
• Verified lightweight bytecode verification

Cited in

(10)

• From flow logic to static type systems for coordination languages
• Program and proof optimizations with type systems
• Bidirectional data flow analysis for type inferencing.
• Fissile type analysis, modular checking of almost everywhere invariants
• Bit-vector typestate analysis
• Tracking data-flow with open closure types
• Dead code elimination based pointer analysis for multithreaded programs
• Recognition of logically related regions based heap abstraction
• Flow analytic type system for array bound checks
• Types from Control Flow Analysis

This page was built for publication: Type systems equivalent to data-flow analyses for imperative languages

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