
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 Tarskistyle...

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 generalpurpose 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 subparadigm 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...

SternBrocot Tree
 Referenced in 3 articles
[sw28560]
 formalise the SternBrocot 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, goaldirected 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...