CIRC
Circ is an automated behavioral prover based on the circularity principle. The circularity principle generalizes both circular coinduction and structural induction and can be expressed in plain English as follows. Assume that each equation of interest (to be proved) e admits a frozen form fr(e) and a set of derived equations, its derivatives, Der(e). The circularity principle requires that the following rule be valid: if from the hypotheses H together with fr(e) we can deduce Der(e), then e is a consequence of H. When fr(e) freezes the equation at the top, the circularity principle becomes circular coinduction. When the equation is frozen at the bottom on a variable, then it becomes a structural induction (on that variable) derivation rule. This way, Circ supports both coinduction and induction as projections of a more general principle.
Keywords for this software
References in zbMATH (referenced in 25 articles , 2 standard articles )
Showing results 1 to 20 of 25.
Sorted by year (- Babenyshev, Sergey; Martins, Manuel A.: Behavioral equivalence of hidden $k$-logics: an abstract algebraic approach (2016)
- Rot, Jurriaan; Bonsangue, Marcello; Rutten, Jan: Proving language inclusion and equivalence by coinduction (2016)
- Lucanu, Dorel; Rusu, Vlad: Program equivalence by circular reasoning (2015)
- Pattinson, Dirk; Schröder, Lutz: Sound and complete equational reasoning over comodels (2015)
- Diaconescu, Răzvan; Ţuţu, Ionuţ: Foundations for structuring behavioural specifications (2014)
- Martins, M.A.; Madeira, A.; Barbosa, L.S.: A coalgebraic perspective on logical interpretations (2013)
- Rot, Jurriaan; Bonsangue, Marcello; Rutten, Jan: Coinductive proof techniques for language equivalence (2013)
- Winter, Joost: Qstream: a suite of streams (2013)
- Bonchi, Filippo; Bonsangue, Marcello; Caltais, Georgiana; Rutten, Jan; Silva, Alexandra: Final semantics for decorated traces (2012)
- Lescanne, Pierre; Perrinel, Matthieu: “Backward” coinduction, Nash equilibrium and the rationality of escalation (2012)
- Roşu, Grigore; Ştefănescu, Andrei: Towards a unified theory of operational and axiomatic semantics (2012)
- Silva, Alexandra: A specification language for Reo connectors (2012)
- Bonsangue, Marcello; Caltais, Georgiana; Goriac, Eugen-Ioan; Lucanu, Dorel; Rutten, Jan; Silva, Alexandra: A decision procedure for bisimilarity of generalized regular expressions (2011)
- Capretta, Venanzio: Coalgebras in functional programming and type theory (2011)
- Silva, Alexandra; Bonchi, Filippo; Bonsangue, Marcello; Rutten, Jan: Quantitative Kleene coalgebras (2011)
- Zantema, Hans; Endrullis, Jörg: Proving equality of streams automatically (2011)
- Capretta, Venanzio: Bisimulations generated from corecursive equations (2010)
- Niqui, Milad; Rutten, Jan: Sampling, splitting and merging in coinductive stream calculus (2010)
- Popescu, Andrei; Gunter, Elsa L.: Incremental pattern-based coinduction for process algebra and its Isabelle formalization (2010)
- Zantema, Hans: Well-definedness of streams by transformation and termination (2010)