scientific article; zbMATH DE number 7649978

DOI10.4230/LIPICS.ITP.2019.29MaRDI QIDQ5875441FDOQ5875441

Authors: Enrico Tassi 

Publication date: 3 February 2023

Title of this publication is not available (Why is that?)

zbMATH Keywords

inductionCoqcontainersequality testparametricity translation

Mathematics Subject Classification ID

Cites Work

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

Cited In (4)

• Title not available (Why is that?)
• 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

Uses Software

• Coq
• Isabelle/HOL
• Matita
• 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)