Pages that link to "Item:Q5549412"

The following pages link to Proving Properties of Programs by Structural Induction (Q5549412):

Displaying 48 items.

• A survey of state vectors (Q458456) (← links)
• Synthesis of list algorithms by mechanical proving (Q485837) (← links)
• An experimental logic based on the fundamental deduction principle (Q580998) (← links)
• Compilation of the ELECTRE reactive language into finite transition systems (Q673127) (← links)
• Natural termination (Q673622) (← links)
• Structural induction in institutions (Q719243) (← links)
• Proofs by induction in equational theories with constructors (Q789177) (← links)
• Inheritance hierarchies: Semantics and unifications (Q1124313) (← links)
• Mechanizing structural induction. I: Formal system (Q1134540) (← links)
• Mechanizing structural induction. II: Strategies (Q1134541) (← links)
• On the algebra of order (Q1143782) (← links)
• The Schorr-Waite marking algorithm revisited (Q1146527) (← links)
• Programs as partial graphs. I: Flow equivalence and correctness (Q1168723) (← links)
• Context induction: A proof principle for behavioural abstractions and algebraic implementations (Q1179807) (← links)
• A semi-algorithm for algebraic implementation proofs (Q1199928) (← links)
• Consistency in networks of relations (Q1231783) (← links)
• The correctness of the Schorr-Waite list marking algorithm (Q1250706) (← links)
• On some classes of interpretations (Q1251892) (← links)
• Proving termination of (conditional) rewrite systems. A semantic approach (Q1323317) (← links)
• Equivalence of formal semantics definition methods (Q1355752) (← links)
• A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names. (Q1401936) (← links)
• An adaptive subdivision method for root finding of univariate polynomials (Q1736361) (← links)
• A strong restriction of the inductive completion procedure (Q1824381) (← links)
• Recursion induction principle revisited (Q1838286) (← links)
• On the applicability of the longest-match rule in lexical analysis. (Q1872687) (← links)
• The origins of structural operational semantics (Q1878710) (← links)
• Reasoning with conditional axioms (Q1924731) (← links)
• Formalization of universal algebra in Agda (Q2333322) (← links)
• The mechanisation of Barendregt-style equational proofs (the residual perspective) (Q2841232) (← links)
• Implementation of proof schemes in the method of invariant transformations (Q3034853) (← links)
• A combinatory account of internal structure (Q3173527) (← links)
• Types in Programming Languages, Between Modelling, Abstraction, and Correctness (Q3188252) (← links)
• Translation Correctness for First-Order Object-Oriented Pattern Matching (Q3498433) (← links)
• Algebra of programming in Agda: Dependent types for relational program derivation (Q3644935) (← links)
• Current methods for proving program correctness (Q3911363) (← links)
• Recursive data structures (Q4055171) (← links)
• (Q4184287) (← links)
• Proving ground confluence and inductive validity in constructor based equational specifications (Q5044723) (← links)
• Topics in termination (Q5055795) (← links)
• Proof systems for structured algebraic specifications: An overview (Q5055918) (← links)
• Proving and rewriting (Q5096184) (← links)
• Induction using term orderings (Q5210765) (← links)
• Mechanizable inductive proofs for a class of ∀ ∃ formulas (Q5210766) (← links)
• Design strategies for rewrite rules (Q5881289) (← links)
• Programming language semantics: It’s easy as 1,2,3 (Q6065508) (← links)
• Folding left and right matters: Direct style, accumulators, and continuations (Q6099203) (← links)
• A theorem prover for a computational logic (Q6488518) (← links)
• Abstract execution (Q6535957) (← links)