@Proceedings{herbelin_et_al:LIPIcs.TYPES.2014, title = {{LIPIcs, Volume 39, TYPES'14, Complete Volume}}, booktitle = {20th International Conference on Types for Proofs and Programs (TYPES 2014)}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-88-0}, ISSN = {1868-8969}, year = {2015}, volume = {39}, editor = {Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014}, URN = {urn:nbn:de:0030-drops-55047}, doi = {10.4230/LIPIcs.TYPES.2014}, annote = {Keywords: Applicative (Functional) Programming, Software/Program Verification, Specifying and Verifying and Reasoning about Programs, Mathematical Logic} }