scientific article; zbMATH DE number 6797262

DOI10.23638/LMCS-13(4:1)2017zbMath1459.03013arXiv1612.02462MaRDI QIDQ5371043

Thorsten Altenkirch, Ambrus Kaposi

Publication date: 24 October 2017

Full work available at URL: https://arxiv.org/abs/1612.02462

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

zbMATH Keywords

dependent typeslogical relationsnormalisation by evaluationinternal type theory

Mathematics Subject Classification ID

Presheaves and sheaves, stacks, descent conditions (category-theoretic aspects) (18F20) Type theory (03B38)

Related Items (7)

The construction of set-truncated higher inductive types ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Normalization by evaluation for modal dependent type theory ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ A presheaf model of parametric type theory ⋮ Pointers in Recursion: Exploring the Tropics

Uses Software

• Agda

This page was built for publication: