Program development schemata as derived rules

DOI10.1006/jsco.1999.0346zbMath1015.68176OpenAlexW2057756105MaRDI QIDQ1583853

Penny Anderson, David A. 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

zbMATH Keywords

theorem provingIsabelle

Mathematics Subject Classification ID

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Program development by specification and transformation. The PROSPECTRA methodology, language family, and system
• A fast pattern matching algorithm derived by transformational and assertional reasoning
• Foundation of logic programming based on inductive definition
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Proving and applying program transformations expressed with second-order patterns
• Isabelle. A generic theorem prover
• The foundation of a generic theorem prover
• The promotion and accumulation strategies in transformational programming
• Derivation of Logic Programs
• A framework for defining logics
• The Semantics of Predicate Logic as a Programming Language
• Natural deduction as higher-order resolution
• 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
• The Equivalence of Certain Computations
• Program development by stepwise refinement
• Fixpoint approach to the theory of computation

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