Artifact Description

Authors:

TLThéo Laurent
Théo Laurent
MLMeven Lennon-Bertrand
Meven Lennon-Bertrand
KMKenji Maillard
Kenji Maillard

Open Access

Publisher website

Google Scholar

5 April 2024

book chapter
Published by Springer Nature

p. 332-337
DOI:10.1007/978-3-031-57262-3_14

Abstract

This document describes the Coq formalisation accompanying the paper Definitional Functoriality for Dependent (Sub)Types, more specifically the content of section 4.

Keywords

DEFINITIONAL FUNCTORIALITY
ARTIFACT DESCRIPTION
COQ FORMALISATION
DOCUMENT DESCRIBES
FORMALISATION ACCOMPANYING
TYPES
DEFINITIONAL
DEPENDENT
DESCRIPTION
COQ

This publication has 2 references indexed in Scilit:

Martin-Löf à la Coq
2024
Decidability of conversion for type theory in type theory
Proceedings of the ACM on Programming Languages, 2017