Proving Properties of Programs by Structural Induction
From MaRDI portal
Publication:5549412
DOI10.1093/comjnl/12.1.41zbMath0164.46202OpenAlexW2159709550WikidataQ56168941 ScholiaQ56168941MaRDI QIDQ5549412
Publication date: 1969
Published in: The Computer Journal (Search for Journal in Brave)
Full work available at URL: https://semanticscholar.org/paper/b3fe91923c1356a8c6dee2c725dd11fcbfeae903
Related Items
On the applicability of the longest-match rule in lexical analysis., Design strategies for rewrite rules, The origins of structural operational semantics, Proving ground confluence and inductive validity in constructor based equational specifications, A combinatory account of internal structure, Topics in termination, Proof systems for structured algebraic specifications: An overview, Equivalence of formal semantics definition methods, Types in Programming Languages, Between Modelling, Abstraction, and Correctness, Inheritance hierarchies: Semantics and unifications, Reasoning with conditional axioms, Proving and rewriting, Mechanizing structural induction. I: Formal system, Mechanizing structural induction. II: Strategies, Translation Correctness for First-Order Object-Oriented Pattern Matching, Unnamed Item, Programming language semantics: It’s easy as 1,2,3, Folding left and right matters: Direct style, accumulators, and continuations, On the algebra of order, A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names., The Schorr-Waite marking algorithm revisited, Recursive data structures, A survey of state vectors, Programs as partial graphs. I: Flow equivalence and correctness, Context induction: A proof principle for behavioural abstractions and algebraic implementations, Synthesis of list algorithms by mechanical proving, An adaptive subdivision method for root finding of univariate polynomials, Compilation of the ELECTRE reactive language into finite transition systems, Natural termination, A semi-algorithm for algebraic implementation proofs, Implementation of proof schemes in the method of invariant transformations, Consistency in networks of relations, Structural induction in institutions, An experimental logic based on the fundamental deduction principle, The correctness of the Schorr-Waite list marking algorithm, On some classes of interpretations, Induction using term orderings, Mechanizable inductive proofs for a class of ∀ ∃ formulas, Algebra of programming in Agda: Dependent types for relational program derivation, Current methods for proving program correctness, A strong restriction of the inductive completion procedure, The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective), Recursion induction principle revisited, Formalization of universal algebra in Agda, Proofs by induction in equational theories with constructors, Proving termination of (conditional) rewrite systems. A semantic approach
