scientific article; zbMATH DE number 4006266

zbMATH Open0621.03040MaRDI QIDQ3757915FDOQ3757915

Authors: Michael Beeson 

Publication date: 1986

Title of this publication is not available (Why is that?)

Recommendations

• Constructive Mathematics and Functional Programming (Abstract)
• Proving and programming
• scientific article; zbMATH DE number 3859117
• scientific article
• scientific article

zbMATH Keywords

constructive type theoryPeano ArithmeticTuring Machinecomputer programmingconstrutive mathematicstype-free logical systems

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Second- and higher-order arithmetic and fragments (03F35)

Cited In (31)

• Full operational set theory with unbounded existential quantification and power set
• Proof of Correctness of Decision Table Programs
• Applicative theories for logarithmic complexity classes
• Formal proof of a program: find
• What Is the Difference Between Proofs and Programs?
• Programming as a mathematical exercise
• Explicit mathematics: power types and overloading
• Proving and programming
• Proof checking and logic programming
• Proofs as programs
• Title not available (Why is that?)
• Partial Horn logic and Cartesian categories
• Proofs and programs
• Proof methods of declarative properties of definite programs
• On Feferman's operational set theory \textsf{OST}
• Writing programs that construct proofs
• Title not available (Why is that?)
• Towards a computation system based on set theory
• A proof-theoretic characterization of the basic feasible functionals
• The Suslin operator in applicative theories: its proof-theoretic analysis via ordinal theories
• The provably terminating operations of the subsystem PETJ of explicit mathematics
• Realizability interpretation of generalized inductive definitions
• Proving properties of Pascal programs in MIZAR 2
• Theories with self-application and computational complexity.
• Title not available (Why is that?)
• The mathematical construction of a program
• From programming-by-example to proving-by-example
• Type theory and proof processing systems
• Operational closure and stability
• Title not available (Why is that?)
• A Proof-Theoretic Account of Programming and the Role of Reduction Rules

This page was built for publication:

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