Paper: A Modality for Recursion (at LICS 2000)
Authors: Hiroshi NakanoAbstract
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.
BibTeX
@InProceedings{Nakano-AModalityforRecursi, author = {Hiroshi Nakano}, title = {A Modality for Recursion}, booktitle = {Proceedings of the Fifteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2000}, year = 2000, editor = {Martin Abadi}, month = {June}, pages = {255--266}, location = {Santa Barbara, CA, USA}, publisher = {IEEE Computer Society Press} }