Program and proof optimizations with type systems
type: Item
instance of: scholarly article
title: Program and proof optimizations with type systems
zbMATH Open document ID: 1151.68008
author: Ando Saabas
author: Tarmo Uustalu
published in: The Journal of Logic and Algebraic Programming
publication date: 2008-11-06T00:00:00Z
Mathematics Subject Classification ID: 68N30
zbMATH DE Number: 5362189
zbMATH Keywords: data-flow analyses
zbMATH Keywords: optimizations
zbMATH Keywords: type systems
zbMATH Keywords: certification
zbMATH Keywords: proof optimization
describes a project that uses: TVOC
MaRDI profile type: Publication
full work available at URL: j.jlap.2008.05.007
OpenAlex ID: W2128433129
cites work: Logic for Programming, Artificial Intelligence, and Reasoning
cites work: Certificate Translation for Optimizing Compilers
cites work: Simple relational correctness proofs for static analyses and program transformations
cites work: Types for Proofs and Programs
cites work: Proof-carrying code from certified abstract interpretation and fixpoint compression
cites work: FM 2005: Formal Methods
cites work: An axiomatic basis for computer programming
cites work: On flow-sensitive security types
cites work: Compiler optimization correctness by temporal logic
cites work: Type systems equivalent to data-flow analyses for imperative languages
cites work: Q4255591
cites work: Q4414732
cites work: A compositional natural semantics and Hoare logic for low-level languages
DOI: 10.1016/J.JLAP.2008.05.007
description: scientific article; zbMATH DE number 5362189