Program and proof optimizations with type systems

DOI10.1016/J.JLAP.2008.05.007MaRDI QIDQ953533zbMATH OpenOpenAlexFDO

Authors Ando Saabas, Tarmo Uustalu

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)

Recommendations

• Simple relational correctness proofs for static analyses and program transformations
• Proof optimization for partial redundancy elimination
• Type systems equivalent to data-flow analyses for imperative languages
• Types for Proofs and Programs
• Refinement types for program analysis

Cites work

• scientific article; zbMATH DE number 1324833 (Why is no real title available?)
• scientific article; zbMATH DE number 1953280 (Why is no real title available?)
• A compositional natural semantics and Hoare logic for low-level languages
• A compositional natural semantics and Hoare logic for low-level languages
• An axiomatic basis for computer programming
• Certificate Translation for Optimizing Compilers
• Compiler optimization correctness by temporal logic
• FM 2005: Formal Methods
• Logic for Programming, Artificial Intelligence, and Reasoning
• Logic for Programming, Artificial Intelligence, and Reasoning
• On flow-sensitive security types
• Proof-carrying code from certified abstract interpretation and fixpoint compression
• Simple relational correctness proofs for static analyses and program transformations
• Type systems equivalent to data-flow analyses for imperative languages
• Types for Proofs and Programs

Cited in

(16)

• Efficient Verified Programs in a Type Theory with Mixed Constructivity
• A compositional natural semantics and Hoare logic for low-level languages
• Simple relational correctness proofs for static analyses and program transformations
• scientific article; zbMATH DE number 1980940 (Why is no real title available?)
• scientific article; zbMATH DE number 2080288 (Why is no real title available?)
• scientific article; zbMATH DE number 683355 (Why is no real title available?)
• Program derivation in type theory: A partitioning problem
• Two algorithms in search of a type-system
• Dead code elimination based pointer analysis for multithreaded programs
• Automated soundness proofs for dataflow analyses and transformations via local rules
• Recognition of logically related regions based heap abstraction
• Proof optimization for partial redundancy elimination
• Relational decomposition
• Optimizing optimal reduction
• Certificates and Separation Logic
• Refinement types for program analysis

Describes a project that uses

Uses Software

• TVOC

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

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