Last update: Sat Jan 6 02:03:49 MST 2018
@Article{Backhouse:1987:WRM,
author = "R. C. Backhouse and A. A. Khamiss",
title = "A While-rule in {Martin-L{\"o}f}'s Theory of Types",
journal = j-COMP-J,
volume = "30",
number = "1",
pages = "27--36",
month = feb,
year = "1987",
CODEN = "CMPJA6",
DOI = "https://doi.org/10.1093/comjnl/30.1.27",
ISSN = "0010-4620 (print), 1460-2067 (electronic)",
ISSN-L = "0010-4620",
MRclass = "68Q99 (03B70 03F50 68N05)",
MRnumber = "88c:68070",
bibdate = "Tue Dec 4 14:48:22 MST 2012",
bibsource = "Compendex database;
Compiler/math.prog.construction.bib;
http://comjnl.oxfordjournals.org/content/30/1.toc;
http://www.math.utah.edu/pub/tex/bib/compj1980.bib;
http://www3.oup.co.uk/computer_journal/hdb/Volume_30/Issue_01/",
URL = "http://comjnl.oxfordjournals.org/content/30/1/27.full.pdf+html;
http://www3.oup.co.uk/computer_journal/hdb/Volume_30/Issue_01/tiff/27.tif;
http://www3.oup.co.uk/computer_journal/hdb/Volume_30/Issue_01/tiff/28.tif;
http://www3.oup.co.uk/computer_journal/hdb/Volume_30/Issue_01/tiff/29.tif;
http://www3.oup.co.uk/computer_journal/hdb/Volume_30/Issue_01/tiff/30.tif;
http://www3.oup.co.uk/computer_journal/hdb/Volume_30/Issue_01/tiff/31.tif;
http://www3.oup.co.uk/computer_journal/hdb/Volume_30/Issue_01/tiff/32.tif;
http://www3.oup.co.uk/computer_journal/hdb/Volume_30/Issue_01/tiff/33.tif;
http://www3.oup.co.uk/computer_journal/hdb/Volume_30/Issue_01/tiff/34.tif;
http://www3.oup.co.uk/computer_journal/hdb/Volume_30/Issue_01/tiff/35.tif;
http://www3.oup.co.uk/computer_journal/hdb/Volume_30/Issue_01/tiff/36.tif",
acknowledgement = ack-nhfb,
affiliation = "Univ of Essex, Colchester, Engl",
affiliationaddress = "Univ of Essex, Colchester, Engl",
classcodes = "C4240 (Programming and algorithm theory); C6110
(Systems analysis and programming)",
classification = "723",
corpsource = "Dept. of Comput. Sci., Essex Univ., Colchester, UK",
fjournal = "The Computer Journal",
journal-URL = "http://comjnl.oxfordjournals.org/",
keywords = "bound functions; computer metatheory --- Programming
Theory; computer programming; intuitionistic theory;
invariant properties; loop; program verification;
programming theory; structures; theory; Theory; theory
of types; type; verification; while-rule;
while-statements",
treatment = "T Theoretical or Mathematical",
}