\texttt{slepice}: towards a verified implementation of type theory in type theory

DOI10.1007/978-3-030-68446-4_7OpenAlexW3130884665MaRDI QIDQ2119108

František Farka

Publication date: 23 March 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-68446-4_7

zbMATH Keywords

dependent typestype inferenceHorn clause logicproof-relevant resolutionterm synthesis

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• Coq
• Ott
• Beluga
• Automath
• Irdis
• CompCert
• TCB
• Idris
• Template-Coq
• ELPI
• MetaCoq

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)