Deprecated: $wgMWOAuthSharedUserIDs=false is deprecated, set $wgMWOAuthSharedUserIDs=true, $wgMWOAuthSharedUserSource='local' instead [Called from MediaWiki\HookContainer\HookContainer::run in /var/www/html/w/includes/HookContainer/HookContainer.php at line 135] in /var/www/html/w/includes/Debug/MWDebug.php on line 372
Shallow embedding of type theory is morally correct - MaRDI portal

Shallow embedding of type theory is morally correct

From MaRDI portal

Publication:2176685

Jump to:navigation, search

DOI10.1007/978-3-030-33636-3_12zbMath1434.03039arXiv1907.07562OpenAlexW2982682917MaRDI QIDQ2176685

András Kovács, Ambrus Kaposi, Nicolai Kraus

Publication date: 5 May 2020

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

zbMATH Keywords

standard model type theory Agda parametricity canonicity shallow embedding set model

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Type theory (03B38)

This page was built for publication: Shallow embedding of type theory is morally correct

Retrieved from "https://portal.mardi4nfdi.de/w/index.php?title=Publication:2176685&oldid=14699251"