Paper Info
Title
Realizability of Monotone Coinductive Definitions and Its Application to Program Synthesis
Abstract
Two realizability interpretations of monotone coinductive definitions are studied. One interpretation is defined so that a realizer of a coinductively defined predicate is the same as that of its expansion. For this interpretation, the paper proves that full monotone coinductive definitions are not sound and restricted monotone coinductive definitions are sound. The other interpreration is based on second order logic and can interpret least-upper-bound coinductive definitions, which is generalization of monotone coinductive definitions. By using these interprerations, the paper shows that a program which treats coinductively defined infinite data structures such as streams can be synthesized from a constructive proof of its specification.
Year
DOI
Venue
1998
10.1007/BFb0054298
MPC
Keywords
Field
DocType
program synthesis,monotone coinductive definitions,second order,data structure,upper bound
Discrete mathematics,Constructive proof,Second-order logic,Program synthesis,Computer science,Coinduction,Data type,Program analysis,Realizability,Monotone polygon
Conference
ISBN
Citations 
PageRank 
3-540-64591-8
5
0.46
References 
Authors
13
1
Name
Order
Citations
PageRank
Makoto Tatsuta111122.36