DocumentCode :
2221991
Title :
A modality for recursion
Author :
Nakano, Hiroshi
Author_Institution :
Ryukoku Univ., Ohtsu, Japan
fYear :
2000
fDate :
2000
Firstpage :
255
Lastpage :
266
Abstract :
We propose a modal logic that enables us to handle self-referential formulae, including ones with negative self-references, which on one hand, would introduce a logical contradiction, namely Russell´s paradox, in the conventional setting, while on the other hand, are necessary to capture a certain class of programs such as fixed point combinators and objects with so-called binary methods in object oriented programming. Our logic provides a basis for axiomatic semantics of such a wider range of programs and a new framework for natural construction of recursive programs in the proofs-as-programs paradigm
Keywords :
formal logic; programming language semantics; theorem proving; type theory; axiomatic semantics; binary methods; fixed point combinators; logical contradiction; modal logic; natural construction; negative self-references; object oriented programming; proofs-as-programs paradigm; recursion; recursive programs; self-referential formulae; Convergence; Data structures; Electronic mail; Logic programming; Network address translation;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Logic in Computer Science, 2000. Proceedings. 15th Annual IEEE Symposium on
Conference_Location :
Santa Barbara, CA
ISSN :
1043-6871
Print_ISBN :
0-7695-0725-5
Type :
conf
DOI :
10.1109/LICS.2000.855774
Filename :
855774
Link To Document :
بازگشت