scientific article; zbMATH DE number 7649978

DOI10.4230/LIPICS.ITP.2019.29MaRDI QIDQ5875441zbMATH OpenFDO

Authors Enrico Tassi

Publication date 3 February 2023

Full work available at URL https://doi.org/10.4230/LIPICS.ITP.2019.29

zbMATH Keywords

containersCoqequality testinductionparametricity translation

Mathematics Subject Classification ID

Cites work

• A syntax for higher inductive-inductive types
• Canonical structures for the working Coq user
• CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions
• First-Class Type Classes
• Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving
• scientific article; zbMATH DE number 1696799 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Parametricity in an impredicative sort
• Programming with higher-order logic.
• The Lean theorem prover (system description)
• The Matita interactive theorem prover
• Truly modular (co)datatypes for Isabelle/HOL
• Type-based termination of generic programs
• Types for Proofs and Programs

Cited in

(8)

• Deep induction: induction rules for (truly) nested types
• Proving tight bounds on univariate expressions with elementary functions in Coq
• scientific article; zbMATH DE number 7649955 (Why is no real title available?)
• A Survey of the Proof-Theoretic Foundations of Logic Programming
• Correct and complete type checking and certified erasure for \textsc{Coq}, in \textsc{Coq}
• Deep induction for inductive families
• Two applications of logic programming to Coq
• Inductive predicates via least fixpoints in higher-order separation logic

Describes a project that uses

Uses Software

• Matita
• Isabelle/HOL
• Coq
• Lean
• ELPI

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5875441)