The Definitional Side of the Forcing
type: Item
instance of: scholarly article
title: The Definitional Side of the Forcing
zbMATH Open document ID: 1394.68063
DOI: 10.1145/2933575.2935320
author: Guilhem Jaber
author: Gabriel Lewertowski
author: Pierre-Marie Pédrot
author: Matthieu Sozeau
author: Nicolas Tabareau
published in: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science
publication date: 2018-04-23T00:00:00Z
Mathematics Subject Classification ID: 68N18
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 03E40
Mathematics Subject Classification ID: 03G30
Mathematics Subject Classification ID: 68N30
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 6863506
zbMATH Keywords: Coq
zbMATH Keywords: dependent type theory
zbMATH Keywords: effects
zbMATH Keywords: forcing
zbMATH Keywords: inductive types
describes a project that uses: Coq
MaRDI profile type: MaRDI publication profile
full work available at URL: https://doi.org/10.1145/2933575.2935320
OpenAlex ID: W2411119043
description: scientific article; zbMATH DE number 6863506