scientific article; zbMATH DE number 7649978

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

Authors Enrico Tassi

Publication date 3 February 2023

zbMATH Keywords

inductionCoqcontainersequality testparametricity translation

Mathematics Subject Classification ID

Cites work

• scientific article; zbMATH DE number 1696799 (Why is no real title available?)
• A syntax for higher inductive-inductive types
• CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions
• Canonical structures for the working Coq user
• First-Class Type Classes
• Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving
• 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

(4)

• scientific article; zbMATH DE number 7649955 (Why is no real title available?)
• Proving tight bounds on univariate expressions with elementary functions in Coq
• Deep induction: induction rules for (truly) nested types
• A Survey of the Proof-Theoretic Foundations of Logic Programming

Describes a project that uses

Uses Software

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

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)