Subset Coercions in Coq
type: Item
instance of: scholarly article
title: Subset Coercions in Coq
zbMATH Open document ID: 1178.68531
DOI: 10.1007/978-3-540-74464-1_16
author: Matthieu Sozeau
published in: Lecture Notes in Computer Science
publication date: 2009-03-10T00:00:00Z
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 5527186
describes a project that uses: PVS
describes a project that uses: Coq
MaRDI profile type: Publication
full work available at URL: 978-3-540-74464-1 16
OpenAlex ID: W1496429054
Recommended article: Q3075242
Recommended article: Q4246948
Recommended article: Q4362923
Recommended article: Inductive and coinductive components of corecursive functions in Coq
Recommended article: From Sets to Bits in Coq
Recommended article: Coercion completion and conservativity in coercive subtyping
Recommended article: Coercive subtyping for the calculus of constructions
Recommended article: Coercive subtyping via mappings of reduction behaviour
Recommended article: Coherence and Transitivity in Coercive Subtyping
Recommended article: Q4499304
description: scientific article