Coinduction (greatest fixed points; bisimilarity; operational interpretation of proofs)

Academic Journals

1. Davide Sangiorgi. On the origins of bisimulation and coinduction. ACM Trans. Program. Lang. Syst, 31(4):1-41, 2009. download
2. Ulrich Berger, Sion Lloyd. A coinductive approach to verified exact real number computation. Electronic Communications of the EASST (ISSN 1863-2122), 23, 2009.
3. Ulrich Berger. Proofs-as-Programs in Computable Analysis. Electronic Communications of the EASST (ISSN 1863-2122), 23, 2009. download
4. C. Grabmayer. A Duality in Proof Systems for Recursive Type Equality and for Bisimulation Equivalence on Cyclic Term Graphs. Electronic Notes in Theoretical Computer Science, 72(1):59-74, 2007.
5. Dexter Kozen. Coinductive Proof Principles for Stochastic Processes. Logical Methods in Computer Science, DOI: 10.2168/LMCS-3 (4:8) 2007, 3(4), 2007.
6. Y. Bertot. CoInduction in Coq. Arxiv preprint cs/0603119, 2006.
7. Luca Aceto, Wan Fokkink, Anna Ingolfsdottir, Sumit Nain. Bisimilarity is not finitely based over BPA with interrupt. Theoretical Computer Science, Algebra and Coalgebra in Computer Science, 366(1):60-81, 2006.
8. Haruo Hosoya, Jerome Vouillon, Benjamin C. Pierce. Regular expression types for XML. ACM Trans. Program. Lang. Syst, 27(1):46-90, 2005. download
9. Jan J. M. M. Rutten. A tutorial on coinductive stream calculus and signal flow graphs. Theor. Comput. Sci, 343(3):443-481, 2005.
10. Hubie Chen, Riccardo Pucella. A coalgebraic approach to Kleene algebra with tests. Theor. Comput. Sci, 327(1):23-44, 2004.
11. Luca Aceto, Zolt\'an Ésik, Anna Ingólfsdóttir. Equational theories of tropical semirings. Theoretical Computer Science, Foundations of Software Science and Computation Structures, 298(3):417-469, 2003.
12. Luca Aceto, Jan Friso Groote. A complete equational axiomatization for MPA with string iteration. Theoretical Computer Science, 211(1):339-374, 1999.
13. Michael Brandt, Fritz Henglein. Coinductive axiomatization of recursive type equality and subtyping. Fundamenta Informaticae, Invited submission to special issue featuring a selection of contributions to the 3d Int'l Conf. on Typed Lambda Calculi and Applications (TLCA), 1997, 33(4):309-338, 1998.
14. Luca Aceto, Anna Ingólfsdóttir. A Characterization of Finitary Bisimulation. Inf. Process. Lett, 64(3):127-134, 1997.
15. Lawrence C. Paulson. Mechanizing Coinduction and Corecursion in Higher-order Logic. J.\ Logic and Computation, 1997.
16. Marcelo P. Fiore. A Coinduction Principle for Recursive Data Types Based on Bisimulation. Information and Computation, Conference version: Proc.\ 8th Annual IEEE Symp.\ on Logic in Computer Science (LICS), 1993, pp.\ 110-119, 127:186-198, 1996.
17. Luca Aceto, Alan Jeffrey. A complete axiomatization of timed bisimulation for a class of timed regular behaviours. Theoretical Computer Science, 152(2):251-268, 1995.
18. Dexter Kozen, Jens Palsberg, Michael Schwartzbach. Efficient Recursive Subtyping. Mathematical Structures in Computer Science (MSCS), Conference version presented at the 20th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages (POPL), 1993, 5(1), 1995.
19. Andrew M. Pitts. A co-inducion principle for recursively defined domains. Theoretical Computer Science (TCS), 124:195-219, 1994.
20. Robin Milner, Mads Tofte. Co-induction in relational semantics. Theoretical Computer Science, Note, 87(1):209-220, 1991.
21. V. Breazu-Tannen, T. Coquand, C. Gunter, A. Scedrov. Inheritance as Implicit Coercion. Information and Computation, Presented at LICS '89, 93(1):172-221, July 1991.
22. Robin Milner. A Complete Axiomatisation for Observational Congruence of Finite-State Behaviors. Information and Computation, 81(2):227-247, May 1989.
23. Robin Milner. A Complete Inference System for a Class of Regular Behaviours. Journal of Computer and System Sciences (JCSS), 28:439-466, 1984.
24. R. Burstall, J. Darlington. A Transformation System for Developing Recursive Programs. J. of the ACM, 24(1):44-67, January 1977.

Book Chapters

1. K. Bruce, P. Wegner. An Algebraic Model of Subtype and Inheritance. F. Bancilhon, P. Buneman (eds.), Chap. 5, pp. 75-96, Frontier Series, Addison-Wesley, ACM Press, 1990.

International Conferences

1. James Brotherston. Formalised Inductive Reasoning in the Logic of Bunched Implications. In SAS, Pages 87-103, 2007.
2. Dexter Kozen, Nicholas Ruozzi. Applications of Metric Coinduction. In Proc. 2nd Conf. Algebra and Coalgebra in Computer Science (CALCO 2007), Mossakowski T. et al. (ed.), Lecture Notes in Computer Science, Volume 4624, Pages 327-341, August 2007.
3. Clemens Grabmayer. Using Proofs by Coinduction to Find ``Traditional'' Proofs. In Proc. 1st Conference on Algebra and Coalgebra in Computer Science (CALCO), Lecture Notes in Computer Science (LNCS), September 2005.
4. Haruo Hosoya, Jerome Vouillon, Benjamin C. Pierce. Regular expression types for XML. In ICFP, Pages 11-22, 2000. download
5. Jan J. M. M. Rutten. Automata and Coinduction (An Exercise in Coalgebra). In CONCUR, Pages 194-218, 1998.
6. Michael Brandt, Fritz Henglein. Coinductive Axiomatization of Recursive Type Equality and Subtyping. In TLCA, Pages 63-81, 1997.
7. Andrew D. Gordon, Gareth D. Rees. Bisimilarity for a First-Order Calculus of Objects with Subtyping. In Proc.\ 23d Annual ACM Symposium on Principles of Programming Languages (POPL), St.\ Petersburg, Florida, Pages 386-395, January 1996.
8. Andrew Gordon. Bisimilarity as a Theory of Functional Programming. In Proceedings of the Eleventh Conference on the Mathematical Foundations of Programming Semantics (MFPS), New Orleans, March 29 to April 1, 1995, Elsevier Electronic Notes in Theoretical Computer Science, volume 1, 1995.
9. Furio Honsell, Marina Lenisa. Final Semantics for untyped lambda-calculus. In Proc.\ Int'l Conf.\ on Typed Lambda Calculi and Applications (TLCA), Mariangiola Dezani-Ciancaglini, Gordon Plotkin (eds.), Lecture Notes in Computer Science (LNCS), Volume 902, Pages 249-265, 1995.
10. David Sands. Total Correctness by Local Improvement in Program Transformation. In Proc. 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Pages 221-232, January 1995.
11. Dexter Kozen, Jens Palsberg, Michael Schwartzbach. Efficient Recursive Subtyping. In Proc. 20th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, Pages 419-428, January 1993.
12. V. Breazu-Tannen, C. Gunter, A. Scedrov. Computing with Coercions. In Proc. ACM Symp. on Lisp and Functional Programming (LFP), Nice, France, M. Wand (ed.), Pages 44-60, 1990.
13. V. Breazu-Tannen, T. Coquand, C. Gunter, A. Scedrov. Inheritance and Explicit Coercion. In Proc. Logic in Computer Science (LICS), Pages 112-129, 1989.
14. David Park. Concurrency and Automata on Infinite Sequences. In Proc.\ 5th GI-Conf.\ Theoretical Computer Science, Karlsruhe, Germany, Lecture Notes in Computer Science (LNCS), Volume 104, Pages 167-183, March 1981.

Technical Reports

1. Dexter Kozen. On the Coalgebraic Theory of Kleene Algebra with Tests. Research Report Computing and Information Science, Cornell University, March 2008.
2. Dexter Kozen, Jens Palsberg, Michael Schwartzbach. Efficient Recursive Subtyping. Research Report DAIMI, Aarhus University, No 0, July 1992.

Miscellaneous

1. Fritz Henglein. Personal communcation with Joshua Auerbach. Email, 1998.
2. David Sands. Total Correctness by Local Improvement in Program Transformation. Manuscript, January 1995.

Master's thesis

1. Michael Brandt. Recursive Subtyping: Axiomatizations and Computational Interpretations. Master's theses DIKU, University of Copenhagen, Universitetsparken 1, DK-2100 Copenhagen, Denmark, April 1997.

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.