Program and proof optimizations with type systems

DOI10.1016/j.jlap.2008.05.007zbMath1151.68008MaRDI QIDQ953533

Tarmo Uustalu, Ando Saabas

Publication date: 6 November 2008

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlap.2008.05.007

zbMATH Keywords

type systems; certification; data-flow analyses; optimizations; proof optimization

Mathematics Subject Classification ID

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Related Items

Proof optimization for partial redundancy elimination, A compositional natural semantics and Hoare logic for low-level languages, Dead code elimination based pointer analysis for multithreaded programs, Recognition of logically related regions based heap abstraction, Certificates and Separation Logic, Relational Decomposition

Uses Software

• TVOC

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proof-carrying code from certified abstract interpretation and fixpoint compression
• Type systems equivalent to data-flow analyses for imperative languages
• A compositional natural semantics and Hoare logic for low-level languages
• Compiler optimization correctness by temporal logic
• Simple relational correctness proofs for static analyses and program transformations
• Certificate Translation for Optimizing Compilers
• On flow-sensitive security types
• An axiomatic basis for computer programming
• Logic for Programming, Artificial Intelligence, and Reasoning
• Logic for Programming, Artificial Intelligence, and Reasoning
• FM 2005: Formal Methods
• Types for Proofs and Programs