{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,31]],"date-time":"2022-03-31T03:03:56Z","timestamp":1648695836150},"reference-count":54,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2013,8,4]],"date-time":"2013-08-04T00:00:00Z","timestamp":1375574400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/2.0"},{"start":{"date-parts":[[2013,8,4]],"date-time":"2013-08-04T00:00:00Z","timestamp":1375574400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/2.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Braz Comput Soc"],"published-print":{"date-parts":[[2013,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>As computer programs become increasingly complex, techniques for ensuring trustworthiness of information manipulated by them become critical. In this work, we use the Coq proof assistant to formalise a <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\lambda $$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03bb<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>-calculus with trust types, originally formulated by \u00d8rb\u00e6k and Palsberg. We give formal proofs of type soundness, erasure and simulation theorems and also prove decidability of the typing problem. As a result of our formalisation a certified type checker is derived.<\/jats:p>","DOI":"10.1007\/s13173-013-0119-5","type":"journal-article","created":{"date-parts":[[2013,8,3]],"date-time":"2013-08-03T05:07:03Z","timestamp":1375506423000},"page":"433-443","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Mechanized metatheory for a $$\\lambda $$-calculus with trust types"],"prefix":"10.1007","volume":"19","author":[{"given":"Rodrigo","family":"Ribeiro","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luc\u00edlia","family":"Figueiredo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carlos","family":"Camar\u00e3o","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,8,4]]},"reference":[{"key":"119_CR1","doi-asserted-by":"crossref","unstructured":"Aydemir BE, Chargu\u00e9raud A, Pierce BC, Pollack R, Weirich S (2008) Engineering formal metatheory. In: Necula GC, Wadler P (eds) POPL. ACM, New York, pp 3\u201315","DOI":"10.1145\/1328897.1328443"},{"key":"119_CR2","unstructured":"Barendrecht HP: The Lambda calculus: its syntax and semantics, studies in logic and the foundations of mathematics, vol 103. Elsevier, New York (1984)"},{"key":"119_CR3","doi-asserted-by":"crossref","unstructured":"Barthe G, Dufay G, Jakubiec L, de Sousa SM (2002) A formal correspondence between offensive and defensive javacard virtual machines. In: Cortesi A (ed) VMCAI, Lecture Notes in Computer Science, vol 2294. Springer, Berlin, pp 32\u201345","DOI":"10.1007\/3-540-47813-2_3"},{"issue":"2","key":"119_CR4","first-page":"35","volume":"33","author":"G Barthe","year":"2007","unstructured":"Barthe G, Rezk T, Basu A (2007) Security types preserving compilation. Computer Lang Syst Struct 33(2):35\u201359","journal-title":"Computer Lang Syst Struct"},{"key":"119_CR5","doi-asserted-by":"crossref","unstructured":"Bertot Y, Cast\u00e9ran P (2004) Interactive theorem proving and program development. Coq\u2019Art: The calculus of inductive constructions. In: Texts in theoretical computer science. Springer, New York","DOI":"10.1007\/978-3-662-07964-5"},{"issue":"3","key":"119_CR6","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10817-009-9148-3","volume":"43","author":"S Blazy","year":"2009","unstructured":"Blazy S, Leroy X (2009) Mechanized semantics for the clight subset of the C language. J Autom Reason 43(3):263\u2013288","journal-title":"J Autom Reason"},{"issue":"5","key":"119_CR7","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"75","author":"N de Bruijn","year":"1972","unstructured":"de Bruijn N (1972) Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church\u2013rosser theorem. Indag Math (Proceedings) 75(5): 381\u2013392. doi:10.1016\/1385-7258(72)90034-0","journal-title":"Indag Math (Proceedings)"},{"issue":"3","key":"119_CR8","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-011-9225-2","volume":"49","author":"A Chargu\u00e9raud","year":"2012","unstructured":"Chargu\u00e9raud A (2012) The locally nameless representation. J Autom Reason 49(3):363\u2013408","journal-title":"J Autom Reason"},{"key":"119_CR9","unstructured":"Arthur C (2013) Locally nameless Coq library. http:\/\/www.chargueraud.org\/softs\/ln\/"},{"key":"119_CR10","doi-asserted-by":"crossref","unstructured":"Chlipala A (2007) A certified type-preserving compiler from lambda calculus to assembly language. In: Ferrante J, McKinley KS (eds) PLDI. ACM, New Yok, pp 54\u201365","DOI":"10.1145\/1273442.1250742"},{"key":"119_CR11","doi-asserted-by":"crossref","unstructured":"Chlipala A (2010) A verified compiler for an impure functional language. In: Hermenegildo MV, Palsberg J (eds) POPL. ACM, New York, pp 93\u2013106","DOI":"10.1145\/1707801.1706312"},{"key":"119_CR12","doi-asserted-by":"crossref","unstructured":"Chlipala A (2011) Mostly-automated verification of low-level programs in computational separation logic. In: Hall MW, Padua DA (eds) PLDI. ACM, New York, pp 234\u2013245","DOI":"10.1145\/1993316.1993526"},{"key":"119_CR13","doi-asserted-by":"crossref","unstructured":"Clarkson MR, Chong S, Myers AC (2008) Civitas: toward a secure voting system. In: IEEE symposium on security and privacy. IEEE Computer Society, Los Alamitos, pp 354\u2013368","DOI":"10.1109\/SP.2008.32"},{"issue":"3","key":"119_CR14","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1145\/1165555.1165572","volume":"37","author":"K Crary","year":"2006","unstructured":"Crary K, Harper R (2006) Higher-order abstract syntax: setting the record straight. SIGACT News 37(3):93\u201396","journal-title":"SIGACT News"},{"issue":"5","key":"119_CR15","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/360051.360056","volume":"19","author":"DE Denning","year":"1976","unstructured":"Denning DE (1976) A lattice model of secure information flow. Commun ACM 19(5):236\u2013243","journal-title":"Commun ACM"},{"key":"119_CR16","unstructured":"Dybvig RK (2009) The Scheme Programming Language, 4th edn. MIT Press, Cambridge"},{"key":"119_CR17","doi-asserted-by":"crossref","unstructured":"Gonthier G (2007) The four colour theorem: engineering of a formal proof. In: Kapur D (ed) ASCM, Lecture notes in computer science, vol 5081. Springer, Heidelberg, p 333","DOI":"10.1007\/978-3-540-87827-8_28"},{"key":"119_CR18","doi-asserted-by":"crossref","unstructured":"Gonthier G (2013) Engineering mathematics: the odd order theorem proof. In: Giacobazzi R, Cousot R (eds) POPL. ACM, New York, pp 1\u20132","DOI":"10.1145\/2480359.2429071"},{"key":"119_CR19","doi-asserted-by":"crossref","unstructured":"Heintze N, Riecke JG (1998) The slam calculus: programming with secrecy and integrity. In: MacQueen DB, Cardelli L (eds) POPL. ACM, New York, pp 365\u2013377","DOI":"10.1145\/268946.268976"},{"key":"119_CR20","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511809835","volume-title":"Lambda-calculus and combinators: an introduction","author":"JR Hindley","year":"2008","unstructured":"Hindley JR, Seldin JP (2008) Lambda-calculus and combinators: an introduction, 2nd edn. Cambridge University Press, New York","edition":"2"},{"key":"119_CR21","unstructured":"Isabelle Team (2013) The archieve of formal proofs. http:\/\/afp.sourceforge.net\/"},{"key":"119_CR22","doi-asserted-by":"crossref","unstructured":"Jones M (1994) Qualified types: theory and practice. PhD thesis. Distinguished Dissertations in Computer Science. Cambridge University Press","DOI":"10.1017\/CBO9780511663086"},{"key":"119_CR23","unstructured":"Jones SP (2003) Haskell 98 language and libraries: the revised report"},{"issue":"3","key":"119_CR24","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/s00165-007-0055-2","volume":"20","author":"F Kamm\u00fcller","year":"2008","unstructured":"Kamm\u00fcller F (2008) Formalizing non-interference for a simple bytecode language in Coq. Formal Asp. Comput. 20(3):259\u2013275","journal-title":"Formal Asp. Comput."},{"issue":"6","key":"119_CR25","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1743546.1743574","volume":"53","author":"G Klein","year":"2010","unstructured":"Klein G, Andronick J, Elphinstone K, Heiser G, Cock D, Derrin P, Elkaduwe D, Engelhardt K, Kolanski R, Norrish M, Sewell T, Tuch H, Winwood S (2010) seL4: formal verification of an operating-system kernel. Commun ACM 53(6):107\u2013115","journal-title":"Commun ACM"},{"key":"119_CR26","doi-asserted-by":"crossref","unstructured":"Kothari S, Caldwell J (2010) A machine checked model of idempotent mgu axioms for lists of equational constraints. In: Fernandez M (ed) Proceedings 24th international workshop on unification, EPTCS, vol 42. pp 24\u201338","DOI":"10.4204\/EPTCS.42.3"},{"issue":"7","key":"119_CR27","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy X (2009) Formal verification of a realistic compiler. Commun ACM 52(7):107\u2013115","journal-title":"Commun ACM"},{"issue":"4","key":"119_CR28","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X Leroy","year":"2009","unstructured":"Leroy X (2009) A formally verified compiler back-end. J Autom Reason 43(4):363\u2013446","journal-title":"J Autom Reason"},{"issue":"1","key":"119_CR29","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-008-9099-0","volume":"41","author":"X Leroy","year":"2008","unstructured":"Leroy X, Blazy S (2008) Formal verification of a C-like memory model and its uses for verifying program transformations. J Autom Reason 41(1):1\u201331","journal-title":"J Autom Reason"},{"key":"119_CR30","volume-title":"Java virtual machine specification","author":"T Lindholm","year":"1999","unstructured":"Lindholm T, Yellin F (1999) Java virtual machine specification, 2nd edn. Addison-Wesley Longman Publishing Co., Inc., Boston","edition":"2"},{"key":"119_CR31","volume-title":"Intuitionistic type theory","author":"P Martin-L\u00f6f","year":"1984","unstructured":"Martin-L\u00f6f P (1984) Intuitionistic type theory. Bibliopolis, Naples"},{"issue":"6","key":"119_CR32","doi-asserted-by":"publisher","first-page":"1061","DOI":"10.1017\/S0956796803004957","volume":"13","author":"C McBride","year":"2003","unstructured":"McBride C (2003) First-order unification by structural recursion. J Funct Program 13(6):1061\u20131075","journal-title":"J Funct Program"},{"key":"119_CR33","doi-asserted-by":"crossref","unstructured":"Morgenstern J, Licata DR (2010) Security-typed programming within dependently-typed programming. In: Proceedings of the International Conference on Functional Programming.","DOI":"10.1145\/1863543.1863569"},{"key":"119_CR34","unstructured":"Myers A et al (1998) Jif Compiler. http:\/\/www.cs.cornell.edu\/jif\/"},{"key":"119_CR35","doi-asserted-by":"crossref","unstructured":"Myers AC (1999) Jflow: practical mostly-static information flow control. In: Appel AW, Aiken A (eds) POPL. ACM, New York, pp 228\u2013241","DOI":"10.1145\/292540.292561"},{"key":"119_CR36","doi-asserted-by":"crossref","unstructured":"Nipkow T, Paulson, LC, Wenzel M (2002) Isabelle\/HOL\u2014a proof assistant for higher-order logic. In: LNCS, vol 2283. Springer, Heidelberg","DOI":"10.1007\/3-540-45949-9"},{"key":"119_CR37","doi-asserted-by":"crossref","unstructured":"Norell U (2009) Dependently typed programming in Agda. In: Kennedy A, Ahmed A (eds) TLDI. ACM, New York, pp 1\u20132","DOI":"10.1007\/978-3-642-04652-0_5"},{"issue":"6","key":"119_CR38","doi-asserted-by":"crossref","first-page":"557","DOI":"10.1017\/S0956796897002906","volume":"7","author":"P \u00d8rb\u00e6k","year":"1997","unstructured":"\u00d8rb\u00e6k P, Palsberg J (1997) Trust in the lambda-calculus. J Funct Program 7(6):557\u2013591","journal-title":"J Funct Program"},{"key":"119_CR39","volume-title":"Types and programming languages","author":"BC Pierce","year":"2002","unstructured":"Pierce BC (2002) Types and programming languages. MIT Press, Cambridge"},{"issue":"2","key":"119_CR40","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0890-5401(03)00138-X","volume":"186","author":"AM Pitts","year":"2003","unstructured":"Pitts AM (2003) Nominal logic, a first order theory of names and binding. Inf Comput 186(2):165\u2013193","journal-title":"Inf Comput"},{"key":"119_CR41","doi-asserted-by":"crossref","unstructured":"Pottier F, Simonet V (2002) Information flow inference for ML. In: Proceedings of the 29th ACM symposium on principles of programming languages. In: (POPL\u201902). Portland, Oregon, pp 319\u2013330","DOI":"10.1145\/503272.503302"},{"key":"119_CR42","doi-asserted-by":"crossref","unstructured":"Pottier F, Simonet V (2003) Information flow inference for ML. ACM transactions on programming languages and systems 25(1):117\u2013158","DOI":"10.1145\/596980.596983"},{"key":"119_CR43","unstructured":"Ribeiro R, et al (2013) A formalization of a lambda-calculus with trust types\u2014on-line repository. https:\/\/github.com\/rodrigogribeiro\/trust-calculus"},{"key":"119_CR44","doi-asserted-by":"crossref","unstructured":"Rimsa A, d\u2019Amorim M, Pereira FMQ (2011) Tainted flow analysis on e-ssa-form programs. In: Knoop J (ed) CC, Lecture notes in computer science, vol 6601. Springer, Berlin, pp 124\u2013143","DOI":"10.1007\/978-3-642-19861-8_8"},{"key":"119_CR45","unstructured":"Jones SP et al (1998) GHC\u2014the Glasgow Haskell Compiler. http:\/\/www.haskell.org\/ghc\/"},{"issue":"1","key":"119_CR46","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","volume":"21","author":"A Sabelfeld","year":"2003","unstructured":"Sabelfeld A, Myers AC (2003) Language-based information-flow security. IEEE J Sel Areas n Commun 21(1):5\u201319","journal-title":"IEEE J Sel Areas n Commun"},{"key":"119_CR47","doi-asserted-by":"crossref","unstructured":"Simonet, V (2003) Type inference with structural subtyping: a faithful formalization of an efficient constraint solver. In: Ohori A (ed) APLAS, Lecture notes in computer science, vol 2895. Springer, Heidelberg, pp 283\u2013302","DOI":"10.1007\/978-3-540-40018-9_19"},{"key":"119_CR48","unstructured":"Snelting G, Wasserrab D (2008) A correctness proof for the Volpano\u2013Smith security typing system. Isabelle Archive of Formal Proofs. http:\/\/afp.sourceforge.net\/entries\/VolpanoSmith.shtml"},{"key":"119_CR49","doi-asserted-by":"crossref","unstructured":"S\u00f8rensen M, Urzyczyn P (2006) Lectures on the Curry\u2013Howard isomorphism. No. v. 10 in studies in logic and the foundations of mathematics. Elsevier, Amsterdam.","DOI":"10.1016\/S0049-237X(06)80005-4"},{"key":"119_CR50","unstructured":"Team IO. Objective Caml (OCaml) programming language website. http:\/\/caml.inria.fr\/"},{"key":"119_CR51","doi-asserted-by":"crossref","unstructured":"Terei D, Mazires D, Marlow S, Jones SP (2012) Safe Haskell. In: Haskell \u201912: proceedings of the fifth ACM SIGPLAN symposium on Haskell. ACM, New York","DOI":"10.1145\/2364506.2364524"},{"issue":"2\u20133","key":"119_CR52","doi-asserted-by":"crossref","first-page":"167","DOI":"10.3233\/JCS-1996-42-304","volume":"4","author":"D Volpano","year":"1996","unstructured":"Volpano D, Irvine C, Smith G (1996) A sound type system for secure flow analysis. J Comput Secur 4(2\u20133):167\u2013187","journal-title":"J Comput Secur"},{"key":"119_CR53","doi-asserted-by":"publisher","unstructured":"Volpano D, Smith G (1997) A type-based approach to program security. In: Lecture notes in computer science, vol 1214, (chap. 48). Springer, Berlin \/ Heidelberg, Berlin\/Heidelberg, pp. 607\u2013621. doi:10.1007\/BFb0030629","DOI":"10.1007\/BFb0030629"},{"issue":"4","key":"119_CR54","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1145\/363516.363520","volume":"9","author":"DS Wallach","year":"2000","unstructured":"Wallach DS, Appel AW, Felten EW (2000) Safkasi: a security mechanism for language-based systems. ACM Trans Softw Eng Methodol 9(4):341\u2013378. doi:10.1145\/363516.363520","journal-title":"ACM Trans Softw Eng Methodol"}],"container-title":["Journal of the Brazilian Computer Society"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s13173-013-0119-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s13173-013-0119-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s13173-013-0119-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s13173-013-0119-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,2]],"date-time":"2021-09-02T00:54:14Z","timestamp":1630544054000},"score":1,"resource":{"primary":{"URL":"https:\/\/journal-bcs.springeropen.com\/articles\/10.1007\/s13173-013-0119-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,8,4]]},"references-count":54,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2013,11]]}},"alternative-id":["119"],"URL":"https:\/\/doi.org\/10.1007\/s13173-013-0119-5","relation":{},"ISSN":["0104-6500","1678-4804"],"issn-type":[{"value":"0104-6500","type":"print"},{"value":"1678-4804","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,8,4]]},"assertion":[{"value":"7 September 2012","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 July 2013","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 August 2013","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}