?url_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Adc&rft.title=Program+Semantics+and+Classical+Logic&rft.creator=Muskens%2C+Reinhard&rft.subject=Language&rft.subject=Logic&rft.description=In+the+tradition+of+Denotational+Semantics+one+usually+lets+program%0Aconstructs+take+their+denotations+in+reflexive+domains%2C+i.e.+in+domains%0Awhere+self-application+is+possible.+For+the+bulk+of+programming%0Aconstructs%2C+however%2C+working+with+reflexive+domains+is+an%0Aunnecessary+complication.+In+this+paper+we+shall+use+the+domains%0Aof+ordinary+classical+type+logic+to+provide+the+semantics+of+a%0Asimple+programming+language+containing+choice+and+recursion.+We+prove%0Athat+the+rule+of+%7B%5Cem+Scott+Induction%5C%2F%7D+holds+in+this+new+setting%2C+prove%0Asoundness+of+a+Hoare+calculus+relative+to+our+semantics%2C+give+a%0Adirect+calculus+%24%7B%5Ccal+C%7D%24+on+programs%2C+and+prove+that+the+denotation+of%0Aany+program+%24P%24+in+our+semantics+is+equal+to+the+union+of+the+denotations%0Aof+all+those+programs+%24L%24+such+that+%24P%24+follows+from+%24L%24+in+our+calculus%0Aand+%24L%24+does+not+contain+recursion+or+choice.&rft.date=1997-01&rft.type=Departmental+Technical+Report&rft.type=NonPeerReviewed&rft.format=application%2Fpostscript&rft.identifier=http%3A%2F%2Fcogprints.org%2F5044%2F1%2Fclassden.ps&rft.format=application%2Fpdf&rft.identifier=http%3A%2F%2Fcogprints.org%2F5044%2F2%2Fclassden.pdf&rft.identifier=++Muskens%2C+Reinhard++(1997)+Program+Semantics+and+Classical+Logic.++%5BDepartmental+Technical+Report%5D++++(Unpublished)++&rft.relation=http%3A%2F%2Fcogprints.org%2F5044%2F