• CIRC

  • Referenced in 40 articles [sw06202]
  • principle. The circularity principle generalizes both circular coinduction and structural induction and can be expressed ... circularity principle becomes circular coinduction. When the equation is frozen at the bottom ... derivation rule. This way, Circ supports both coinduction and induction as projections of a more...
  • Paco

  • Referenced in 16 articles [sw10885]
  • Paco: A Coq Library for Parameterized Coinduction. Paco is a Coq library implementing parameterized coinduction ... Parameterized coinduction is a technique for defining coinductive predicates (i.e., in Prop), using which ... perform coinductive proofs in a more compositional and incremental fashion than with standard Tarski-style...
  • CoALP

  • Referenced in 17 articles [sw16105]
  • Coalgebraic logic programming: from semantics to implementation. Coinductive definitions, such as that of an infinite...
  • Coinductive

  • Referenced in 6 articles [sw28537]
  • Isabelle Coinductive: This article collects formalisations of general-purpose coinductive data types and sets. Currently ... contains coinductive natural numbers, coinductive lists, i.e. lazy lists or streams, infinite streams, coinductive terminated ... lists, coinductive resumptions, a library of operations on coinductive lists, and a version of König ... lemma as an application for coinductive lists. The initial theory was contributed by Paulson...
  • SafeDpi

  • Referenced in 13 articles [sw01989]
  • contextually defined behavioural equivalence can be characterised coinductively, using bisimulations based on typed actions...
  • Tac

  • Referenced in 7 articles [sw09455]
  • automatically proving many theorems using induction and coinduction. Since the automatic proof procedure is structured...
  • CoCaml

  • Referenced in 3 articles [sw22657]
  • CoCaml: functional programming with regular coinductive types. Functional languages offer a high level of abstraction ... development of functional programming are inductive and coinductive types and associated programming constructs, such ... well supported in most languages, coinductive types are subject of more recent research ... define recursive functions on regular coinductive datatypes. These functions are defined like usual recursive functions...
  • Kumo

  • Referenced in 5 articles [sw06963]
  • equational logic are implemented, including induction and coinduction. Kumo generates proof documentation...
  • coFJ

  • Referenced in 5 articles [sw29270]
  • extension to Featherweight Java that promotes coinductive programming, a sub-paradigm expressly devised to ease...
  • CoCLAM

  • Referenced in 2 articles [sw28719]
  • failure to generate witnesses for coinduction from divergent proof attempts. Coinduction is a proof rule ... central difficulty in the automation of coinductive proof is the choice of a relation (called ... bisimulation). We present an automation of coinductive theorem proving. This automation is based ... guess, so that a larger class of coinductive problems can be automatically verified. The implementation...
  • Stern-Brocot Tree

  • Referenced in 3 articles [sw28560]
  • formalise the Stern-Brocot tree as a coinductive tree using recursive and iterative specifications, which...
  • Stream Fusion Code

  • Referenced in 1 article [sw28590]
  • list functions in the theories List and Coinductive_List, and prove them correct with respect ... that end, it covers both finite and coinductive lists from the HOL library ... Coinductive entry. The fusible list functions require specification and proof principles different from Huffman...
  • Galliwasp

  • Referenced in 2 articles [sw09566]
  • down, goal-directed manner using coinduction. Galliwasp next checks if the candidate answer sets...
  • Qstream

  • Referenced in 1 article [sw13491]
  • Haskell, QStream, implementing the technique of coinductive counting by making use of Haskell’s built ... coinduction capabilities. We furthermore provide a number of useful tools for stream exploration, including...
  • Codatatype

  • Referenced in 1 article [sw28678]
  • definitions by corecursion and proofs by coinduction. Regular operations on languages are then defined ... standard definitions). As an exercise in coinduction we also prove the axioms of Kleene algebra...
  • Dynamic Architectures

  • Referenced in 1 article [sw30953]
  • traces, they are formalized in terms of coinductive lists. Thus, our theory is based ... Lochbihler’s formalization of coinductive lists. The theory may be applied to verify properties...
  • Abstract Soundness

  • Referenced in 1 article [sw28839]
  • Abstract Soundness. A formalized coinductive account of the abstract development of Brotherston, Gorogiannis, and Petersen...
  • Coq

  • Referenced in 1751 articles [sw00161]
  • Coq is a formal proof management system. It...
  • CUTE

  • Referenced in 58 articles [sw00177]
  • CUTE: a concolic unit testing engine for C...
  • FEPG

  • Referenced in 4 articles [sw00276]
  • The finite element program generator (FEPG) is a...