Paco
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.
Keywords for this software
References in zbMATH (referenced in 20 articles , 1 standard article )
Showing results 1 to 20 of 20.
Sorted by year (- Letan, Thomas; Régis-Gianas, Yann; Chifflier, Pierre; Hiet, Guillaume: Modular verification of programs with effects and effects handlers (2021)
- Madiot, Jean-Marie; Pous, Damien; Sangiorgi, Davide: Modular coinduction up-to for higher-order languages via first-order transition systems (2021)
- Rusu, Vlad; Nowak, David: (Co)inductive proof systems for compositional proofs in reachability logic (2021)
- Abel, Andreas; Allais, Guillaume; Hameer, Aliya; Pientka, Brigitte; Momigliano, Alberto; Schäfer, Steven; Stark, Kathrin: POPLMark reloaded: mechanizing proofs by logical relations (2019)
- Dagnino, Francesco: Coaxioms: flexible coinductive definitions by inference systems (2019)
- Pous, Damien; Sangiorgi, Davide: Bisimulation and coinduction enhancements: a historical perspective (2019)
- Hasuo, Ichiro; Kataoka, Toshiki; Cho, Kenta: Coinductive predicates and final sequences in a fibration (2018)
- Ancona, Davide; Dagnino, Francesco; Zucca, Elena: Generalizing inference systems by coaxioms (2017)
- Bach Poulsen, Casper; Mosses, Peter D.: Flag-based big-step semantics (2017)
- Blanchette, Jasmin Christian; Bouzy, Aymeric; Lochbihler, Andreas; Popescu, Andrei; Traytel, Dmitriy: Friends with benefits. Implementing corecursion in foundational proof assistants (2017)
- Pous, Damien; Rot, Jurriaan: Companions, codensity and causality (2017)
- Schäfer, Steven; Smolka, Gert: Tower induction and up-to techniques for CCS with fixed points (2017)
- Abel, Andreas: Compositional coinduction with sized types (2016)
- Bengtson, Jesper; Parrow, Joachim; Weber, Tjark: Psi-calculi in Isabelle (2016)
- Devesas Campos, Marco; Fiore, Marcelo: Classical logic with Mendler induction -- a dual calculus and its strong normalization (2016)
- Ziliani, Beta; Dreyer, Derek; Krishnaswami, Neelakantan R.; Nanevski, Aleksandar; Vafeiadis, Viktor: Mtac: a monad for typed tactic programming in Coq (2015)
- Anand, Abhishek; Rahli, Vincent: Towards a formally verified proof assistant (2014)
- Endrullis, Jörg; Hendriks, Dimitri; Bodin, Martin: Circular coinduction in Coq using bisimulation-up-to techniques (2013)
- Hasuo, Ichiro; Cho, Kenta; Kataoka, Toshiki: Coinductive predicates and final sequences in a fibration (2013)
- Hur, Chung-Kil; Neis, Georg; Dreyer, Derek; Vafeiadis, Viktor: The power of parameterization in coinductive proof (2013)