Proving Properties of Programs by Structural Induction

Cited in

(52)

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

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)