Output details
11 - Computer Science and Informatics
University of Dundee
Article title
Inductive and coinductive components of corecursive functions in Coq
Type
D - Journal article
Title of journal
Electronic Notes in Theoretical Computer Science
Article number
-
Volume number
203
Issue number
5
First page of article
25
ISSN of journal
1571-0661
Year of publication
2008
Number of additional authors
1
Additional information
<11> The paper is one of the major outcomes of Komendantskaya's postdoctoral INRIA CORDI fellowship in INRIA, France (2007-2008). Deciding termination of (co)recursive functions is an undecidable problem in general, but the paper proposed a new method to decides termination of a bigger class of corecursive functions in Coq. The results were well received at CMCS’08, TYPES'08, and invited talks at the Centre for Mathematics and Informatics, U.Provence, France and U.StAndrews. As a result, Komendantskaya organised a workshop PAR’10 (with EPTCS proceedings) on this topic at major conference FLoC’10. This work laid foundations for EPSRC grant EP/K031864/1 (£430K).
Interdisciplinary
-
Cross-referral requested
-
Research group
None
Citation count
5
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-
