A While-rule in Martin-Lof's Theory of Types

DOI10.1093/comjnl/30.1.27zbMath0638.03057OpenAlexW2010552804MaRDI QIDQ3778750

A. A. Khamiss, Roland C. Backhouse

Publication date: 1987

Published in: The Computer Journal (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1093/comjnl/30.1.27

zbMATH Keywords

invariant propertiesbound functionsloop structuresintuitionistic theory of typeswhile-statements

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Second- and higher-order arithmetic and fragments (03F35)

Related Items (3)

Constructing recursion operators in intuitionistic type theory ⋮ Computing downwards accumulations on trees quickly ⋮ A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction

This page was built for publication: A While-rule in Martin-Lof's Theory of Types