Recursive Programs as Definitions in First-Order Logic

DOI10.1137/0213026MaRDI QIDQ5184385zbMATH OpenOpenAlexFDO

Authors Robert Cartwright

Publication date 1984

Published in SIAM Journal on Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1137/0213026

zbMATH Keywords

first order logicfixed- point theory of recursive programshigher order logicprogram logicprogram transformationsrewrite rulessemanticsverification

Mathematics Subject Classification ID

Higher-type and set recursion theory (03D65) Abstract and axiomatic computability and recursion theory (03D75) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Recommendations

• scientific article; zbMATH DE number 4210120
• scientific article; zbMATH DE number 3903941
• Recursive programs and denotational semantics in absolute logics of programs
• scientific article; zbMATH DE number 51768
• Logic programs and recursion

Cited in

(10)

• Hoare's logic for nondeterministic regular programs: A nonstandard approach
• Recursive programs and denotational semantics in absolute logics of programs
• A formalization of programs in first-order logic with a discrete linear order
• Reductional programming of functions represented by recurrent relations of the first order
• Logic programs and recursion
• scientific article; zbMATH DE number 3903941 (Why is no real title available?)
• Unbounded program memory adds to the expressive power of first-order programming logic
• What is a universal higher-order programming language?
• scientific article; zbMATH DE number 3892565 (Why is no real title available?)
• Total correctness in nonstandard logics of programs

Describes a project that uses

Uses Software

• LCF

This page was built for publication: Recursive Programs as Definitions in First-Order Logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5184385)