Program and proof optimizations with type systems

DOI10.1016/J.JLAP.2008.05.007zbMATH Open1151.68008OpenAlexW2128433129MaRDI QIDQ953533FDOQ953533

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

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

zbMATH Keywords

type systemscertificationdata-flow analysesoptimizationsproof optimization

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• An axiomatic basis for computer programming
• Types for Proofs and Programs
• A compositional natural semantics and Hoare logic for low-level languages
• Simple relational correctness proofs for static analyses and program transformations
• On flow-sensitive security types
• Logic for Programming, Artificial Intelligence, and Reasoning
• FM 2005: Formal Methods
• Title not available (Why is that?)
• Certificate Translation for Optimizing Compilers
• Logic for Programming, Artificial Intelligence, and Reasoning
• 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

Cited In (13)

• Relational Decomposition
• Title not available (Why is that?)
• Proof optimization for partial redundancy elimination
• Efficient Verified Programs in a Type Theory with Mixed Constructivity
• Title not available (Why is that?)
• Two algorithms in search of a type-system
• A compositional natural semantics and Hoare logic for low-level languages
• Optimizing optimal reduction
• Title not available (Why is that?)
• Dead code elimination based pointer analysis for multithreaded programs
• Recognition of logically related regions based heap abstraction
• Certificates and Separation Logic
• Program derivation in type theory: A partitioning problem

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)