Reus, Bernhard ;
Streicher, Thomas
Relative Completeness for Logics of Functional Programs
Abstract
We prove a relative completeness result for a logic of functional programs extending D. Scott's LCF. For such a logic, contrary to results for Hoare logic, it does not make sense to ask whether it is complete relative to the full theory of its firstorder part, since the first order part does not determine uniquely the model at higherorder types. Therefore, one has to fix a model and choose an appropriate data theory w.r.t. which the logic is relatively complete. We establish relative completeness for two models: for the Scott model we use the theory of Baire Space as data theory, and for the effective Scott model we take firstorder arithmetic. In both cases we need to extend traditional LCF in order to capture a sufficient amount of domain theory.
BibTeX  Entry
@InProceedings{reus_et_al:LIPIcs:2011:3250,
author = {Bernhard Reus and Thomas Streicher},
title = {{Relative Completeness for Logics of Functional Programs}},
booktitle = {Computer Science Logic (CSL'11)  25th International Workshop/20th Annual Conference of the EACSL},
pages = {470480},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897323},
ISSN = {18688969},
year = {2011},
volume = {12},
editor = {Marc Bezem},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2011/3250},
URN = {urn:nbn:de:0030drops32509},
doi = {http://dx.doi.org/10.4230/LIPIcs.CSL.2011.470},
annote = {Keywords: completeness, program logics, LCF}
}
2011
Keywords: 

completeness, program logics, LCF 
Seminar: 

Computer Science Logic (CSL'11)  25th International Workshop/20th Annual Conference of the EACSL

Related Scholarly Article: 


Issue date: 

2011 
Date of publication: 

2011 