Proof-assistants using dependent type systems
From MaRDI portal
Recommendations
- scientific article; zbMATH DE number 6296049
- An introduction to programming and proving with dependent types in Coq
- Type theories from Barendregt's cube for theorem provers
- Crafting a Proof Assistant
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
Cited in
(30)- Proof assistants: history, ideas and future
- N. G. de Bruijn (1918--2012) and his road to Automath, the earliest proof checker
- Classical \(F_{\omega}\), orthogonality and symmetric candidates
- Fiat: deductive synthesis of abstract data types in a proof assistant
- A framework for defining logical frameworks
- Inductive and coinductive components of corecursive functions in Coq
- Dependently Typed Programming Based on Automated Theorem Proving
- An introduction to programming and proving with dependent types in Coq
- A module calculus for Pure Type Systems
- Crafting a Proof Assistant
- Local Theory Specifications in Isabelle/Isar
- scientific article; zbMATH DE number 683355 (Why is no real title available?)
- Cut Elimination in a Class of Sequent Calculi for Pure Type Systems
- Characteristics of de Bruijn’s early proof checker Automath
- Introduction to Type Theory
- Type theories from Barendregt's cube for theorem provers
- The challenge of computer mathematics
- Mtac: a monad for typed tactic programming in Coq
- scientific article; zbMATH DE number 6296049 (Why is no real title available?)
- Machine-checked security proofs of cryptographic signature schemes
- Primitive Floats in Coq
- Proof-term synthesis on dependent-type systems via explicit substitutions
- Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants
- scientific article; zbMATH DE number 7756106 (Why is no real title available?)
- Formalizing two-level type theory with cofibrant exo-nat
- Pure type systems without explicit contexts
- Some probabilistic riddles and some logical solutions
- Computer theorem proving in mathematics
- Obituary: Nicolaas Govert de Bruijn (1918--2012). Mathematician, computer scientist, logician
- N. G. de Bruijn's contribution to the formalization of mathematics
This page was built for publication: Proof-assistants using dependent type systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2751370)
