Go to the corresponding LIPIcs Volume Portal 
pdfformat: 

@InProceedings{krivine:LIPIcs:2015:5495, author = {JeanLouis Krivine}, title = {{On the Structure of Classical Realizability Models of ZF}}, booktitle = {20th International Conference on Types for Proofs and Programs (TYPES 2014)}, pages = {146161}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {9783939897880}, ISSN = {18688969}, year = {2015}, volume = {39}, editor = {Hugo Herbelin and Pierre Letouzey and Matthieu Sozeau}, publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik}, address = {Dagstuhl, Germany}, URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5495}, URN = {urn:nbn:de:0030drops54953}, doi = {10.4230/LIPIcs.TYPES.2014.146}, annote = {Keywords: lambdacalculus, CurryHoward correspondence, set theory} }
Keywords:  lambdacalculus, CurryHoward correspondence, set theory  
Seminar:  20th International Conference on Types for Proofs and Programs (TYPES 2014)  
Issue Date:  2015  
Date of publication:  29.09.2015 