Proving Properties of Programs by Structural Induction

Cited in

(52)

Inheritance hierarchies: Semantics and unifications
Mechanizing structural induction. I: Formal system
Mechanizing structural induction. II: Strategies
On the algebra of order
The Schorr-Waite marking algorithm revisited
Programs as partial graphs. I: Flow equivalence and correctness
Context induction: A proof principle for behavioural abstractions and algebraic implementations
A semi-algorithm for algebraic implementation proofs
Consistency in networks of relations
The correctness of the Schorr-Waite list marking algorithm
On some classes of interpretations
Proving termination of (conditional) rewrite systems. A semantic approach
Equivalence of formal semantics definition methods
A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
An adaptive subdivision method for root finding of univariate polynomials
A strong restriction of the inductive completion procedure
Recursion induction principle revisited
On the applicability of the longest-match rule in lexical analysis.
The origins of structural operational semantics
Reasoning with conditional axioms
Formalization of universal algebra in Agda
The mechanisation of Barendregt-style equational proofs (the residual perspective)
Implementation of proof schemes in the method of invariant transformations
A combinatory account of internal structure
Types in programming languages, between modelling, abstraction, and correctness (extended abstract)
Translation Correctness for First-Order Object-Oriented Pattern Matching
Algebra of programming in Agda: Dependent types for relational program derivation
Current methods for proving program correctness
Recursive data structures
scientific article; zbMATH DE number 3621093 (Why is no real title available?)
A survey of state vectors
Synthesis of list algorithms by mechanical proving
Proving ground confluence and inductive validity in constructor based equational specifications
Topics in termination
Proof systems for structured algebraic specifications: An overview
Proving and rewriting
Induction using term orderings
Mechanizable inductive proofs for a class of \(\forall \exists\) formulas
An experimental logic based on the fundamental deduction principle
Design strategies for rewrite rules
Programming language semantics: It’s easy as 1,2,3
Folding left and right matters: Direct style, accumulators, and continuations
A theorem prover for a computational logic
Abstract execution
Compilation of the ELECTRE reactive language into finite transition systems
Natural termination
Rod Burstall: in memoriam (1934--2025)
A unified view of induction reasoning for first-order logic
A contextual formalization of structural coinduction
Syntax monads for the working formal metatheorist
Structural induction in institutions
Proofs by induction in equational theories with constructors

This page was built for publication: Proving Properties of Programs by Structural Induction

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