High-Level Theories
From MaRDI portal
Publication:5505502
DOI10.1007/978-3-540-85110-3_19zbMath1166.68338OpenAlexW2132124019WikidataQ60712741 ScholiaQ60712741MaRDI QIDQ5505502
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
Related Items
Theory morphisms in Church's type theory with quotation and evaluation ⋮ Formalizing mathematical knowledge as a biform theory graph: a case study ⋮ Theory Presentation Combinators ⋮ Incorporating quotation and evaluation into Church's type theory ⋮ MathScheme: Project Description ⋮ Realms: A Structure for Consolidating Knowledge about Mathematical Theories
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Multi-stage programming with functors and monads: eliminating abstraction overhead from generic code
- \textit{Theorema}: Towards computer-aided mathematical theory exploration
- The calculus of constructions
- Isabelle. A generic theorem prover
- Theorem proving modulo
- An overview of a formal framework for managing mathematics
- Gaussian elimination: a case study in efficient genericity with MetaOCaml
- Building Decision Procedures in the Calculus of Inductive Constructions
- A Rational Reconstruction of a System for Experimental Mathematics
- Biform Theories in Chiron
- Certified Computer Algebra on Top of an Interactive Theorem Prover
