scientific article; zbMATH DE number 7649978

DOI10.4230/LIPIcs.ITP.2019.29MaRDI QIDQ5875441

Enrico Tassi

Publication date: 3 February 2023

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

inductionCoqcontainersequality testparametricity translation

Mathematics Subject Classification ID

Related Items (3)

A Survey of the Proof-Theoretic Foundations of Logic Programming ⋮ Unnamed Item ⋮ Deep induction: induction rules for (truly) nested types

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Type-based termination of generic programs
• Isabelle/HOL. A proof assistant for higher-order logic
• Truly Modular (Co)datatypes for Isabelle/HOL
• Programming with Higher-Order Logic
• Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving
• The Lean Theorem Prover (System Description)
• First-Class Type Classes
• A Syntax for Higher Inductive-Inductive Types
• The Matita Interactive Theorem Prover
• Canonical Structures for the Working Coq User
• CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions
• Types for Proofs and Programs

This page was built for publication: