High-Level Theories
From MaRDI portal
Publication:5505502
DOI10.1007/978-3-540-85110-3_19zbMATH Open1166.68338DBLPconf/aisc/CaretteF08OpenAlexW2132124019WikidataQ60712741 ScholiaQ60712741MaRDI QIDQ5505502FDOQ5505502
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
Recommendations
Cites Work
- Isabelle. A generic theorem prover
- Title not available (Why is that?)
- The calculus of constructions
- Theorem proving modulo
- Title not available (Why is that?)
- \textit{Theorema}: Towards computer-aided mathematical theory exploration
- Certified Computer Algebra on Top of an Interactive Theorem Prover
- Gaussian elimination: a case study in efficient genericity with MetaOCaml
- Multi-stage programming with functors and monads: eliminating abstraction overhead from generic code
- Ascertaining mathematical theorems
- Title not available (Why is that?)
- Title not available (Why is that?)
- Biform Theories in Chiron
- An overview of a formal framework for managing mathematics
- Building Decision Procedures in the Calculus of Inductive Constructions
- A Rational Reconstruction of a System for Experimental Mathematics
Cited In (8)
- Theory presentation combinators
- Incorporating quotation and evaluation into Church's type theory
- MathScheme: project description
- Theory morphisms in Church's type theory with quotation and evaluation
- Higher Lawvere theories
- First order meta theories
- Realms: a structure for consolidating knowledge about mathematical theories
- Formalizing mathematical knowledge as a biform theory graph: a case study
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)
