Program development schemata as derived rules

DOI10.1006/JSCO.1999.0346zbMATH Open1015.68176OpenAlexW2057756105MaRDI QIDQ1583853FDOQ1583853

Authors: Penny Anderson, David Basin 

Publication date: 27 February 2002

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/8e476c9c78b856a8e42473746b418aa1a81cca40

Recommendations

• A logic for schema-based program development
• scientific article; zbMATH DE number 954242
• scientific article; zbMATH DE number 42961
• scientific article; zbMATH DE number 46336
• scientific article; zbMATH DE number 177458
• An abstract formalization of correct schemas for program synthesis

zbMATH Keywords

theorem provingIsabelle

Mathematics Subject Classification ID

Cites Work

• Title not available (Why is that?)
• Isabelle. A generic theorem prover
• A framework for defining logics
• Title not available (Why is that?)
• Program development by stepwise refinement
• The Semantics of Predicate Logic as a Programming Language
• A fast pattern matching algorithm derived by transformational and assertional reasoning
• Fixpoint approach to the theory of computation
• Title not available (Why is that?)
• Title not available (Why is that?)
• Proving and applying program transformations expressed with second-order patterns
• Title not available (Why is that?)
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Natural deduction as higher-order resolution
• The foundation of a generic theorem prover
• Derivation of Logic Programs
• Title not available (Why is that?)
• Title not available (Why is that?)
• Program development by specification and transformation. The PROSPECTRA methodology, language family, and system
• The promotion and accumulation strategies in transformational programming
• Foundation of logic programming based on inductive definition
• The Equivalence of Certain Computations
• Title not available (Why is that?)
• Synthesis and transformation of logic programs using unfold/fold proofs
• A survey of GCLA: a definitional approach to logic programming
• Logic programming, functional programming, and inductive definitions
• A fixedpoint approach to implementing (co)inductive definitions

Cited In (8)

• Title not available (Why is that?)
• A logic for schema-based program development
• An abstract formalization of correct schemas for program synthesis
• Uniform schemata for proof rules
• Title not available (Why is that?)
• Analogical program derivation based on type theory
• Program abstraction and instantiation
• Title not available (Why is that?)

Uses Software

• Isabelle
• TAS
• Isabelle/ZF
• Nuprl
• Automath
• KIDS
• Elf

This page was built for publication: Program development schemata as derived rules

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