Pages that link to "Item:Q2751370"
From MaRDI portal
The following pages link to Proof-assistants using dependent type systems (Q2751370):
Displaying 24 items.
- Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants (Q597106) (← links)
- Computer theorem proving in mathematics (Q704001) (← links)
- Obituary: Nicolaas Govert de Bruijn (1918--2012). Mathematician, computer scientist, logician (Q740456) (← links)
- N. G. de Bruijn's contribution to the formalization of mathematics (Q740481) (← links)
- Proof assistants: history, ideas and future (Q1040001) (← links)
- N. G. de Bruijn (1918--2012) and his road to Automath, the earliest proof checker (Q1935352) (← links)
- Classical \(F_{\omega}\), orthogonality and symmetric candidates (Q2482840) (← links)
- Fiat: deductive synthesis of abstract data types in a proof assistant (Q2819861) (← links)
- A framework for defining logical frameworks (Q2864157) (← links)
- Inductive and coinductive components of corecursive functions in Coq (Q2873661) (← links)
- Dependently Typed Programming Based on Automated Theorem Proving (Q2908568) (← links)
- Crafting a Proof Assistant (Q3612433) (← links)
- Local Theory Specifications in Isabelle/Isar (Q3638251) (← links)
- (Q4312475) (← links)
- Cut Elimination in a Class of Sequent Calculi for Pure Type Systems (Q4924532) (← links)
- Characteristics of de Bruijn’s early proof checker Automath (Q5089679) (← links)
- Introduction to Type Theory (Q5191087) (← links)
- The challenge of computer mathematics (Q5301849) (← links)
- Mtac: A monad for typed tactic programming in Coq (Q5371944) (← links)
- (Q5417200) (← links)
- Machine-Checked Security Proofs of Cryptographic Signature Schemes (Q5862663) (← links)
- Primitive Floats in Coq (Q5875413) (← links)
- Proof-term synthesis on dependent-type systems via explicit substitutions (Q5958764) (← links)
- (Q6079227) (← links)
