Representing proof transformations for program optimization

DOI10.1007/3-540-58156-1_42zbMath1433.68091OpenAlexW2075909731MaRDI QIDQ5210798

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)

Related Items

Representing proof transformations for program optimization, Proof-search in type-theoretic languages: An introduction, The practice of logical frameworks

Uses Software

• Coq
• ML
• Nuprl
• Elf

Cites Work

• Proving and applying program transformations expressed with second-order patterns
• Implementing tactics and tacticals in a higher-order logic programming language
• The promotion and accumulation strategies in transformational programming
• Finite Differencing of Computable Expressions
• A framework for defining logics
• A Transformation System for Developing Recursive Programs
• Introduction to generalized type systems
• A logic programming language with lambda-abstraction, function variables, and simple unification
• Representing proof transformations for program optimization
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item