\texttt{slepice}: towards a verified implementation of type theory in type theory
From MaRDI portal
Publication:2119108
DOI10.1007/978-3-030-68446-4_7OpenAlexW3130884665MaRDI QIDQ2119108
Publication date: 23 March 2022
Full work available at URL: https://doi.org/10.1007/978-3-030-68446-4_7
Uses Software
Cites Work
- Unnamed Item
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Towards certified meta-programming with typed Template-Coq
- A trustworthy proof checker
- Nominal unification
- The \textsc{MetaCoq} project
- Operational semantics of resolution and productivity in Horn clause logic
- Mechanizing the metatheory of LF
- ELPI: Fast, Embeddable, $$\lambda $$ Prolog Interpreter
- Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis
- Some logical and syntactical observations concerning the first-order dependent type system λP
- An insider's look at LF type reconstruction: everything you (n)ever wanted to know
- Ott
- Implementing type theory in higher order constraint logic programming
- On equivalence and canonical forms in the LF type theory
- Idris, a general-purpose dependently typed programming language: Design and implementation
- Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
