High-Level Theories

DOI10.1007/978-3-540-85110-3_19MaRDI QIDQ5505502zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Jacques Carette, William M. Farmer

Publication date 27 January 2009

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-85110-3_19

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Building Structured Theories
• The mathematical construction of a program
• Theories as types
• scientific article; zbMATH DE number 4039334
• Introducing basic theories for the foundations of mathematics

Cites work

• scientific article; zbMATH DE number 1086637 (Why is no real title available?)
• scientific article; zbMATH DE number 5494025 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• scientific article; zbMATH DE number 4189687 (Why is no real title available?)
• A Rational Reconstruction of a System for Experimental Mathematics
• An overview of a formal framework for managing mathematics
• Ascertaining mathematical theorems
• Biform Theories in Chiron
• Building Decision Procedures in the Calculus of Inductive Constructions
• Certified Computer Algebra on Top of an Interactive Theorem Prover
• Gaussian elimination: a case study in efficient genericity with MetaOCaml
• Isabelle. A generic theorem prover
• Multi-stage programming with functors and monads: eliminating abstraction overhead from generic code
• The calculus of constructions
• Theorem proving modulo
• \textit{Theorema}: Towards computer-aided mathematical theory exploration

Cited in

(8)

• MathScheme: project description
• Realms: a structure for consolidating knowledge about mathematical theories
• First order meta theories
• Higher Lawvere theories
• Theory presentation combinators
• Incorporating quotation and evaluation into Church's type theory
• Formalizing mathematical knowledge as a biform theory graph: a case study
• Theory morphisms in Church's type theory with quotation and evaluation

This page was built for publication: High-Level Theories

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