Program and proof optimizations with type systems

DOI10.1016/J.JLAP.2008.05.007zbMath1151.68008OpenAlexW2128433129MaRDI 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 systemscertificationdata-flow analysesoptimizationsproof optimization

Mathematics Subject Classification ID

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

Related Items (6)

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 ⋮ Relational Decomposition ⋮ Certificates and Separation Logic

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

This page was built for publication: Program and proof optimizations with type systems