Journal article icon

Journal article

Reasoning about codata

Abstract:

Programmers happily use induction to prove properties of recursive programs. To show properties of corecursive programs they employ coinduction, but perhaps less enthusiastically. Coinduction is often considered a rather low-level proof method, in particular, as it departs quite radically from equational reasoning. Corecursive programs are conveniently defined using recursion equations. Suitably restricted, these equations possess unique solutions. Uniqueness gives rise to a simple and attrac...

Expand abstract

Actions


Access Document


Publisher copy:
10.1007/978-3-642-17685-2_3

Authors


Journal:
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume:
6299 LNCS
Pages:
42-93
Publication date:
2010
DOI:
EISSN:
1611-3349
ISSN:
0302-9743
URN:
uuid:90628842-22b0-4dec-88ed-e58c1c2d4ab8
Source identifiers:
328733
Local pid:
pubs:328733
Language:
English

Terms of use


Metrics



If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP