Coq as a Metatheory for Nuprl with Bar Induction

Unpublished conference/Abstract (Scientific congresses, symposiums and conference proceedings)

RAHLI, Vincent; Bickford, Mark

2015 • Continuity, Computability, Constructivity – From Logic to Algorithms (CCC 2015)

Permalink
https://hdl.handle.net/10993/22650

barind-CCC2015.pdf

Author preprint (101.99 kB)

All documents in ORBilu are protected by a user license.

Disciplines :

Computer science

Author, co-author :

RAHLI, Vincent ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT)

Bickford, Mark; Cornell University > Computer Science Department

External co-authors :

yes

Language :

English

Title :

Coq as a Metatheory for Nuprl with Bar Induction

Publication date :

2015

Event name :

Continuity, Computability, Constructivity – From Logic to Algorithms (CCC 2015)

Event date :

September 2015

Commentary :

Presented at CCC 2015 (http://www.nuprl.org/html/Nuprl2Coq/)

Available on ORBilu :

since 30 November 2015

Number of views

108 (34 by Unilu)

Number of downloads

79 (0 by Unilu)