A necessary and sufficient condition in order that a Herbrand interpretation be expressive relative to recursive programs
From MaRDI portal
Publication:3332239
DOI10.1016/S0019-9958(83)80006-0zbMath0543.68022MaRDI QIDQ3332239
Publication date: 1983
Published in: Information and Control (Search for Journal in Brave)
Hoare logicHerbrand interpretationrecursive programexpressive interpretationnatural chainstrongly arithmetical interpretation
Model theory (03C99) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) General topics in the theory of software (68N01)
Related Items (5)
Some relationships between logics of programs and complexity theory ⋮ On the expressive power of finitely typed and universally polymorphic recursive procedures ⋮ Semantics and reasoning with free procedures ⋮ Reasoning about procedures as parameters in the language L4 ⋮ Necessary and sufficient conditions for the universality of programming formalisms
This page was built for publication: A necessary and sufficient condition in order that a Herbrand interpretation be expressive relative to recursive programs