Constructive Mathematics and Functional Programming (Abstract)

DOI10.1007/978-3-540-78739-6_12MaRDI QIDQ5458392zbMATH OpenOpenAlexFDO

Authors Thierry Coquand

Publication date 11 April 2008

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-78739-6_12

Mathematics Subject Classification ID

Other constructive mathematics (03F65) Functional programming and lambda calculus (68N18)

Recommendations

• Constructive Mathematics in Theory and Programming Practice
• scientific article; zbMATH DE number 3859117
• scientific article; zbMATH DE number 3936476
• Reading between the lines in constructive type theory
• Propositions and specifications of programs in Martin-Löf's type theory

Cites work

• A compiled implementation of strong reduction
• A Modular Formalisation of Finite Group Theory
• A monadic, functional implementation of real numbers
• A proof of strong normalisation using domain theory
• Affine functions and series with co-inductive real numbers
• Design and formal proof of a new optimal image segmentation program with hypermaps
• scientific article; zbMATH DE number 3859117 (Why is no real title available?)
• scientific article; zbMATH DE number 3325567 (Why is no real title available?)
• New Computational Paradigms
• The Four Colour Theorem: Engineering of a Formal Proof
• The Mechanical Evaluation of Expressions

Cited in

(24)

• A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
• Proof theory and computer programming
• scientific article; zbMATH DE number 3881865 (Why is no real title available?)
• scientific article; zbMATH DE number 3850461 (Why is no real title available?)
• scientific article; zbMATH DE number 3859117 (Why is no real title available?)
• RZ: a Tool for Bringing Constructive and Computable Mathematics Closer to Programming Practice
• The Constructive Hilbert Program and the Limits of Martin-Löf Type Theory
• scientific article; zbMATH DE number 3936476 (Why is no real title available?)
• scientific article; zbMATH DE number 3952752 (Why is no real title available?)
• scientific article; zbMATH DE number 4006266 (Why is no real title available?)
• scientific article; zbMATH DE number 4091490 (Why is no real title available?)
• scientific article; zbMATH DE number 4123726 (Why is no real title available?)
• Constructive Mathematics in Theory and Programming Practice
• scientific article; zbMATH DE number 1302056 (Why is no real title available?)
• scientific article; zbMATH DE number 599579 (Why is no real title available?)
• Reading between the lines in constructive type theory
• scientific article; zbMATH DE number 4116496 (Why is no real title available?)
• Domain-specific languages of mathematics
• scientific article; zbMATH DE number 3894466 (Why is no real title available?)
• Real and ideal in constructive mathematics
• Program testing and the meaning explanations of intuitionistic type theory
• RZ: A Tool for Bringing Constructive and Computable Mathematics Closer to Programming Practice
• Propositions and specifications of programs in Martin-Löf's type theory
• A computer-verified monadic functional implementation of the integral

This page was built for publication: Constructive Mathematics and Functional Programming (Abstract)

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