ScienceOpen:
research and publishing network
For Publishers
Discovery
Metadata
Peer review
Hosting
Publishing
For Researchers
Join
Publish
Review
Collect
My ScienceOpen
Sign in
Register
Dashboard
Blog
About
Search
Advanced search
My ScienceOpen
Sign in
Register
Dashboard
Search
Search
Advanced search
For Publishers
Discovery
Metadata
Peer review
Hosting
Publishing
For Researchers
Join
Publish
Review
Collect
Blog
About
48
views
11
references
Top references
cited by
4
Cite as...
0 reviews
Review
0
comments
Comment
0
recommends
+1
Recommend
0
collections
Add to
0
shares
Share
Twitter
Sina Weibo
Facebook
Email
3,116
similar
All similar
Record
: found
Abstract
: not found
Book Chapter
: not found
Types for Proofs and Programs
The Not So Simple Proof-Irrelevant Model of CC
other
Author(s):
Alexandre Miquel
,
Benjamin Werner
Publication date
(Online):
April 15 2003
Publisher:
Springer Berlin Heidelberg
Read this book at
Publisher
Buy book
Review
Review book
Invite someone to review
Bookmark
Cite as...
There is no author summary for this book yet. Authors can add summaries to their books on ScienceOpen to make them more accessible to a non-specialist audience.
Related collections
Cancer Immunotherapy
Most cited references
11
Record
: found
Abstract
: not found
Article
: not found
The calculus of constructions
Thierry Coquand
,
Gérard Huet
(1988)
0
comments
Cited
99
times
– based on
0
reviews
Review now
Bookmark
Record
: found
Abstract
: not found
Book Chapter
: not found
Polymorphism is not set-theoretic
John Reynolds
(1984)
0
comments
Cited
12
times
– based on
0
reviews
Bookmark
Record
: found
Abstract
: not found
Book Chapter
: not found
Sets in types, types in sets
Benjamin Werner
(1997)
0
comments
Cited
9
times
– based on
0
reviews
Bookmark
All references
Author and book information
Book Chapter
Publication date (Print):
2003
Publication date (Online):
April 15 2003
Pages
: 240-258
DOI:
10.1007/3-540-39185-1_14
SO-VID:
18e430b3-145a-4898-a21a-96ac7211164a
History
Data availability:
Comments
Comment on this book
Sign in to comment
Book chapters
pp. 259
Structured Proofs in Isar/HOL
pp. 148
A Unifying Approach to Recursive and Co-recursive Definitions
pp. 200
A New Extraction for Coq
pp. 240
The Not So Simple Proof-Irrelevant Model of CC
Similar content
3,116
Resolution-optimized NMR measurement of (1)D(CH), (1)D(CC) and (2)D(CH) residual dipolar couplings in nucleic acid bases.
Authors:
Stuart L. Bryce
,
Carol E. O’Neil
,
Ad Bax
…
Recent advancements in dehydrogenative cross coupling reactions for CC bond formation
Authors:
Begur Vasanthkumar Varun
,
Jayaraman Dhineshkumar
,
Kiran Bettadapur
…
Characterization of donor dendritic cells and enhancement of dendritic cell efflux with CC-chemokine ligand 21: a novel strategy to prolong islet allograft survival.
Authors:
Andrea Vergani
,
Cay von Seydewitz
,
Andrea Augello
…
See all similar
Cited by
3
The Implicit Calculus of Constructions as a Programming Language with Dependent Types
Authors:
Bruno Barras
,
Bruno Bernardo
Subset Coercions in Coq
Authors:
Matthieu Sozeau
Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC)
Authors:
Amin Timany
,
Matthieu Sozeau
See all cited by