Software Search - zbMATH Open

Paco

swMATH ID:	10885
Software Authors:	Chung-Kil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis
Description:	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 one can perform coinductive proofs in a more compositional and incremental fashion than with standard Tarski-style constructions. The Paco library provides a tactic called ”pcofix”, replacing Coq’s primitive cofix and avoiding its syntactic guardedness checking of proof terms. We have found that pcofix yields clear performance and usability benefits, even on simple examples.
Homepage:	http://plv.mpi-sws.org/paco/
Related Software:	Coq; Isabelle/HOL; Agda; Isabelle; coFJ; CoCaml; Archive Formal Proofs; MiniAgda; GitHub; Haskell; Psi-calculi; Nominal Isabelle; PoplMark; CakeML; AmiCo; Featherweight Java; CompCertTSO; HOL; HOL Light; ML
Cited in:	22 Publications

1 Publication describing the Software, including 1 Publication in zbMATH	Year
The power of parameterization in coinductive proof. Zbl 1301.68220 Hur, Chung-Kil; Neis, Georg; Dreyer, Derek; Vafeiadis, Viktor	2013

all top 5

3	Dagnino, Francesco
3	Pous, Damien
2	Abel, Andreas M.
2	Cho, Kenta
2	Dreyer, Derek R.
2	Hasuo, Ichiro
2	Kataoka, Toshiki
2	Sangiorgi, Davide
2	Schäfer, Steven
2	Vafeiadis, Viktor
1	Allais, Guillaume
1	Anand, Abhishek
1	Ancona, Davide
1	Bach Poulsen, Casper
1	Bengtson, Jesper
1	Biernacki, Dariusz
1	Blanchette, Jasmin Christian
1	Bodin, Martin
1	Bouzy, Aymeric
1	Chifflier, Pierre
1	Devesas Campos, Marco
1	Endrullis, Jörg
1	Fiore, Marcelo P.
1	Hameer, Aliya
1	Hendriks, Dimitri
1	Hiet, Guillaume
1	Hur, Chung-Kil
1	Krishnaswami, Neelakantan R.
1	Lenglet, Sergueï
1	Letan, Thomas
1	Lochbihler, Andreas
1	Madiot, Jean-Marie
1	Momigliano, Alberto
1	Mosses, Peter D.
1	Nanevski, Aleksandar
1	Neis, Georg
1	Nowak, David E.
1	Parrow, Joachim
1	Pientka, Brigitte
1	Polesiuk, Piotr
1	Popescu, Andrei
1	Rahli, Vincent
1	Régis-Gianas, Yann
1	Rot, Jurriaan
1	Rusu, Vlad
1	Smolka, Gert
1	Stark, Kathrin
1	Traytel, Dmitry
1	Weber, Tjark
1	Ziliani, Beta
1	Zucca, Elena

all top 5

3	Logical Methods in Computer Science
2	Formal Aspects of Computing
2	Journal of Functional Programming
2	Journal of Logical and Algebraic Methods in Programming
1	Journal of Automated Reasoning
1	MSCS. Mathematical Structures in Computer Science

21	Computer science (68-XX)
11	Mathematical logic and foundations (03-XX)
3	Order, lattices, ordered algebraic structures (06-XX)
2	Category theory; homological algebra (18-XX)
1	General algebraic systems (08-XX)