Yves Bertot & Pierre Castéran (2004):
Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions.
Texts in Theoretical Computer Science. An EATCS Series.
Springer,
doi:10.1007/978-3-662-07964-5.
Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu & Dmitriy Traytel (2017):
Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants.
In: ESOP,
Lecture Notes in Computer Science 10201.
Springer,
pp. 111–140,
doi:10.1016/0304-3975(91)90043-2.
Ştefan Ciobâcă & Dorel Lucanu (2018):
A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems.
In: IJCAR,
Lecture Notes in Computer Science 10900.
Springer,
pp. 295–311,
doi:10.1016/j.ic.2008.03.026.
Eduardo Giménez (1994):
Codifying Guarded Definitions with Recursive Schemes.
In: TYPES,
Lecture Notes in Computer Science 996.
Springer,
pp. 39–59,
doi:10.1007/3-540-60579-7_3.
C. A. R. Hoare (1969):
An Axiomatic Basis for Computer Programming.
Commun. ACM 12(10),
pp. 576–580,
doi:10.1145/363235.363259.
Chung-Kil Hur, Georg Neis, Derek Dreyer & Viktor Vafeiadis (2013):
The power of parameterization in coinductive proof.
In: POPL.
ACM,
pp. 193–206.
Dorel Lucanu, Vlad Rusu & Andrei Arusoaie (2017):
A generic framework for symbolic execution: A coinductive approach.
J. Symb. Comput. 80,
pp. 125–163,
doi:10.1016/j.jsc.2016.07.012.
Dorel Lucanu, Vlad Rusu, Andrei Arusoaie & David Nowak (2015):
Verifying Reachability-Logic Properties on Rewriting-Logic Specifications.
In: Logic, Rewriting, and Concurrency,
Lecture Notes in Computer Science 9200.
Springer,
pp. 451–474,
doi:10.1007/978-3-319-02654-1_16.
Brandon M. Moore, Lucas Peña & Grigore Rosu (2018):
Program Verification by Coinduction.
In: ESOP,
Lecture Notes in Computer Science 10801.
Springer,
pp. 589–618,
doi:10.1145/2480359.2429093.
Tobias Nipkow, Lawrence C. Paulson & Markus Wenzel (2002):
Isabelle/HOL - A Proof Assistant for Higher-Order Logic.
Lecture Notes in Computer Science 2283.
Springer,
doi:10.1007/3-540-45949-9_6.
Peter W. O'Hearn (2019):
Separation logic.
Commun. ACM 62(2),
pp. 86–95,
doi:10.1145/3211968.
Willem P. de Roever, Frank S. de Boer, Ulrich Hannemann, Jozef Hooman, Yassine Lakhnech, Mannes Poel & Job Zwiers (2001):
Concurrency Verification: Introduction to Compositional and Noncompositional Methods.
Cambridge Tracts in Theoretical Computer Science 54.
Cambridge University Press.
Grigore Rosu, Andrei Stefanescu, Ştefan Ciobâcă & Brandon M. Moore (2013):
One-Path Reachability Logic.
In: LICS.
IEEE Computer Society,
pp. 358–367.
Vlad Rusu, Gilles Grimaud & Michaël Hauspie (2018):
Proving Partial-Correctness and Invariance Properties of Transition-System Models.
In: TASE.
IEEE Computer Society,
pp. 60–67.
Vlad Rusu, Gilles Grimaud & Michaël Hauspie (2019):
Proving Partial-Correctness and Invariance Properties of Transition-System Models.
Available at https://hal.inria.fr/hal-01962912.
Davide Sangiorgi (2011):
Introduction to Bisimulation and Coinduction.
Cambridge University Press,
New York, NY, USA,
doi:10.1017/CBO9780511777110.
Stephen Skeirik, Andrei Stefanescu & José Meseguer (2017):
A Constructor-Based Reachability Logic for Rewrite Theories.
In: LOPSTR,
Lecture Notes in Computer Science 10855.
Springer,
pp. 201–217,
doi:10.1007/978-3-319-08918-8_29.
Andrei Stefanescu, Ştefan Ciobâcă, Radu Mereuta, Brandon M. Moore, Traian-Florin Serbanuta & Grigore Rosu (2019):
All-Path Reachability Logic.
Logical Methods in Computer Science 15(2).
Andrei Stefanescu, Daejun Park, Shijiao Yuwen, Yilong Li & Grigore Rosu (2016):
Semantics-based program verifiers for all languages.
In: OOPSLA.
ACM,
pp. 74–91,
doi:10.1145/2983990.2984027.
eptcs@eptcs.org