{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:15:23Z","timestamp":1725484523816},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540415176"},{"type":"electronic","value":"9783540445579"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44557-9_5","type":"book-chapter","created":{"date-parts":[[2007,5,31]],"date-time":"2007-05-31T23:04:24Z","timestamp":1180652664000},"page":"77-93","source":"Crossref","is-referenced-by-count":1,"title":["Specification of a Smart Card Operating System"],"prefix":"10.1007","author":[{"given":"Gustavo","family":"Betarte","sequence":"first","affiliation":[]},{"given":"Cristina","family":"Cornes","sequence":"additional","affiliation":[]},{"given":"Nora","family":"Szasz","sequence":"additional","affiliation":[]},{"given":"Alvaro","family":"Tasistro","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,6,11]]},"reference":[{"key":"5_CR1","unstructured":"B. Barras et al. The Coq Proof Assistant Reference Manual, Version 6.1. Rapport de recherche 203, INRIA, 1997."},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"D. Bolignano. Towards a Mechanization of Cryptographic Protocol Verification. In 9th. International Computer-Aided Verification Conference, June 1997.","DOI":"10.1007\/3-540-63166-6_15"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"D. Bolignano. Towards the Formal Verification of Electronic Comerce Protocols. In 10th. Computer Security Foundations Workshop, June 1997.","DOI":"10.1109\/CSFW.1997.596802"},{"key":"5_CR4","unstructured":"B. Brock and Jr W. A. Hunt. Report on the Formal Specification and PartialVerification of the VIPER Microprocessor. Technical Report 46, Computational Logic, Inc., January 1990."},{"key":"5_CR5","unstructured":"T. Coquand. Une Th_eorie des Constructions. Th\u00e8se de doctorat, Universit\u00e9 Paris 7, 1985."},{"key":"5_CR6","unstructured":"J.C. Filliatre. Proof of Imperative Programs. In Chapter 18 ofThe Coq Proof Assistant Reference Manual, Version 6.2.4, 1999."},{"key":"5_CR7","unstructured":"E. Gim\u00e9nez. A tutorial on recursive types in coq. Technical Report 0221, INRIA, 1998."},{"key":"5_CR8","unstructured":"J. Gosling, B. Joy, and G. J. Steele. The JavaTM Language Specification. Addison-esley, 1996."},{"key":"5_CR9","unstructured":"P. Martin-L\u00f6f. Intuitionistic Type Theory. Bibliopolis, 1984."},{"key":"5_CR10","unstructured":"J.S. Moore. Mechanically Verified Hardware Implementing an 8-Bit Parallel IO By-zantine Agreement Processor. Technical Report NASA Contractor Report 189588, Computational Logic, Inc., 1992."},{"key":"5_CR11","unstructured":"W. Rankl and W. Effing. Smart Card Handbook. John Wiley & Sons, 1997."},{"key":"5_CR12","unstructured":"Sun Microsystems, Inc. Java Card Technology, 1999. Available in \n                  http:\/\/java.sun.com\/products\/javacard\/\n                  \n                ."}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44557-9_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,16]],"date-time":"2019-02-16T21:46:58Z","timestamp":1550353618000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44557-9_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540415176","9783540445579"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-44557-9_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}