Representing proof transformations for program optimization

DOI10.1007/3-540-58156-1_42MaRDI QIDQ5210798zbMATH OpenOpenAlexFDO

Authors Penny Anderson

Publication date 21 January 2020

Published in Automated Deduction — CADE-12 (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/inria-00074441/file/RR-2229.pdf

Mathematics Subject Classification ID

Logic in computer science (03B70) Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• scientific article; zbMATH DE number 1555192
• scientific article; zbMATH DE number 785053
• scientific article; zbMATH DE number 2185653
• Extraction and verification of programs by analysis of formal proofs
• Analysis of methods for extraction of programs from non-constructive proofs.

Cites work

• A framework for defining logics
• A logic programming language with lambda-abstraction, function variables, and simple unification
• A Transformation System for Developing Recursive Programs
• Finite Differencing of Computable Expressions
• scientific article; zbMATH DE number 4133471 (Why is no real title available?)
• scientific article; zbMATH DE number 3853066 (Why is no real title available?)
• scientific article; zbMATH DE number 4053062 (Why is no real title available?)
• scientific article; zbMATH DE number 3740740 (Why is no real title available?)
• scientific article; zbMATH DE number 65531 (Why is no real title available?)
• scientific article; zbMATH DE number 1348473 (Why is no real title available?)
• Implementing tactics and tacticals in a higher-order logic programming language
• Introduction to generalized type systems
• Proving and applying program transformations expressed with second-order patterns
• Representing proof transformations for program optimization
• The promotion and accumulation strategies in transformational programming

Cited in

(14)

• Recursive program optimization through inductive synthesis proof transformation
• Proof-search in type-theoretic languages: An introduction
• scientific article; zbMATH DE number 2185653 (Why is no real title available?)
• scientific article; zbMATH DE number 2185700 (Why is no real title available?)
• scientific article; zbMATH DE number 1555192 (Why is no real title available?)
• scientific article; zbMATH DE number 2090315 (Why is no real title available?)
• On the Proof Theory of Program Transformations
• Program derivation with verified transformations — a case study
• From Verification to Optimizations
• Representing proof transformations for program optimization
• Generating compiler optimizations from proofs
• Formal program optimization in Nuprl using computational equivalence and partial types
• The practice of logical frameworks
• Logical query optimization by proof-tree transformation

Describes a project that uses

Uses Software

• Elf
• Nuprl
• Coq
• ML

This page was built for publication: Representing proof transformations for program optimization

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