{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,26]],"date-time":"2024-08-26T21:46:59Z","timestamp":1724708819528},"reference-count":76,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2012,3,1]],"date-time":"2012-03-01T00:00:00Z","timestamp":1330560000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2016,3,1]],"date-time":"2016-03-01T00:00:00Z","timestamp":1456790400000},"content-version":"vor","delay-in-days":1461,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Applied Logic"],"published-print":{"date-parts":[[2012,3]]},"DOI":"10.1016\/j.jal.2011.12.002","type":"journal-article","created":{"date-parts":[[2011,12,23]],"date-time":"2011-12-23T20:43:22Z","timestamp":1324673002000},"page":"92-114","source":"Crossref","is-referenced-by-count":26,"title":["A modal type theory for formalizing trusted communications"],"prefix":"10.1016","volume":"10","author":[{"given":"Giuseppe","family":"Primiero","sequence":"first","affiliation":[]},{"given":"Mariarosaria","family":"Taddeo","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.jal.2011.12.002_br0010","series-title":"Proceedings 15th Int. Workshop on Computer Science Logic, CSL\u02bc01","first-page":"292","article-title":"Categorical and Kripke semantics for constructive S4 modal logic","author":"Alechina","year":"2001"},{"issue":"2","key":"10.1016\/j.jal.2011.12.002_br0020","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1016\/0168-0072(94)90007-8","article-title":"Logic of proofs","volume":"67","author":"Artemov","year":"1994","journal-title":"Annals of Pure and Applied Logic"},{"issue":"1","key":"10.1016\/j.jal.2011.12.002_br0030","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2687821","article-title":"Explicit provability and constructive semantics","volume":"7","author":"Artemov","year":"2001","journal-title":"Bulletin of Symbolic Logic"},{"issue":"1","key":"10.1016\/j.jal.2011.12.002_br0040","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1016\/j.tcs.2006.03.009","article-title":"Justified common knowledge","volume":"357","author":"Artemov","year":"2006","journal-title":"Theoretical Computer Science"},{"issue":"6","key":"10.1016\/j.jal.2011.12.002_br0050","doi-asserted-by":"crossref","first-page":"1059","DOI":"10.1093\/logcom\/exi053","article-title":"Introducing justification to epistemic logic","volume":"15","author":"Artemov","year":"2005","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/j.jal.2011.12.002_br0060","first-page":"405","article-title":"The place of testimony in the fabric of justification and knowledge","volume":"34","author":"Audi","year":"1997","journal-title":"American Philosophical Quarterly"},{"key":"10.1016\/j.jal.2011.12.002_br0070","series-title":"Moral Prejudices","article-title":"Sustaining trust","author":"Baier","year":"1994"},{"key":"10.1016\/j.jal.2011.12.002_br0080","series-title":"Proceedings of TARK\u02bc98, Seventh Conference on Theoretical Aspects of Rationality and Knowledge","first-page":"43","article-title":"The logic of public announcements, common knowledge and private suspicions","author":"Baltag","year":"1998"},{"key":"10.1016\/j.jal.2011.12.002_br0090","series-title":"Logic and the Foundations of Game and Decision Theory","first-page":"9","article-title":"A qualitative theory of dynamic interactive belief revision","volume":"vol. 3","author":"Baltag","year":"2008"},{"key":"10.1016\/j.jal.2011.12.002_br0100","unstructured":"A. Baltag, S. Smets, Talking Your Way into Agreement: Belief Merge by Persuasive Communication, in: CEUR Workshop Proceedings, vol. 494, Proceedings of the Second Multi-Agent Logics, Languages, and Organisations Federated Workshops, Turin, Italy, September 7\u201310, 2009, 2009, pp. 129\u2013141."},{"key":"10.1016\/j.jal.2011.12.002_br0110","series-title":"Ambient Intelligence","first-page":"308","article-title":"Distributed defeasible contextual reasoning in ambient computing","volume":"vol. 5355","author":"Bikakis","year":"2008"},{"key":"10.1016\/j.jal.2011.12.002_br0120","doi-asserted-by":"crossref","first-page":"363","DOI":"10.2307\/2026823","article-title":"Epistemic tit for tat","volume":"84","author":"Blais","year":"1987","journal-title":"Journal of Philosophy"},{"key":"10.1016\/j.jal.2011.12.002_br0130","doi-asserted-by":"crossref","unstructured":"J. Broersen, M. Dastani, Z. Huang, L.W.N. van der Torre, Trust and commitment in dynamic logic, in: Proceedings of the First EurAsian Conference on Information and Communication Technology, October 29\u201331, 2002, pp. 677\u2013684.","DOI":"10.1007\/3-540-36087-5_79"},{"key":"10.1016\/j.jal.2011.12.002_br0140","unstructured":"S. Buva\u010d, Quantificational logic of context, in: Proceedings of the Thirteenth National Conference on Artificial Intelligence, 1996, pp. 600\u2013606."},{"issue":"3","key":"10.1016\/j.jal.2011.12.002_br0150","first-page":"412","article-title":"Metamathematics of contexts","volume":"23","author":"Buva\u010d","year":"1995","journal-title":"Fundamenta Informaticae"},{"key":"10.1016\/j.jal.2011.12.002_br0160","doi-asserted-by":"crossref","unstructured":"M. Carbone, M. Nielsen, V. Sassone, A formal model for trust in dynamic networks, in: Proc. of IEEE International Conference on Software Engineering and Formal Methods (SEFM\u02bc03), 2003.","DOI":"10.1109\/SEFM.2003.1236207"},{"key":"10.1016\/j.jal.2011.12.002_br0170","doi-asserted-by":"crossref","unstructured":"M. Carbone, M. Nielsen, V. Sassone, A calculus of trust management, in: Proceedings from Foundations of Software Technology and Theoretical Computer Science, 24th International Conference (FSTTCS\u02bc04), 2004.","DOI":"10.1007\/978-3-540-30538-5_14"},{"key":"10.1016\/j.jal.2011.12.002_br0180","article-title":"Trust Mediation in Knowledge Management and Sharing","volume":"vol. 2995","author":"Castelfranchi","year":"2004"},{"key":"10.1016\/j.jal.2011.12.002_br0190","series-title":"Trust Theory. A Socio-Cognitive and Computational Model","author":"Castelfranchi","year":"2010"},{"key":"10.1016\/j.jal.2011.12.002_br0200","series-title":"Procs. of Fifth Workshop on Computational Logic in Multi-Agent Systems (CLIMA V)","first-page":"144","article-title":"Inferring trust","volume":"vol. 3487","author":"Dastani","year":"2004"},{"key":"10.1016\/j.jal.2011.12.002_br0210","article-title":"Reasoning about Trust: A Formal Logic Framework","volume":"vol. 2995","author":"Demolombe","year":"2004"},{"key":"10.1016\/j.jal.2011.12.002_br0220","article-title":"Dynamic Epistemic Logic","volume":"vol. 337","author":"van Ditmarsch","year":"2006"},{"key":"10.1016\/j.jal.2011.12.002_br0230","series-title":"Types for Proofs and Programs","first-page":"63","article-title":"On the logical content of computational type theory: A solution to Curry\u02bcs problem","volume":"vol. 2277","author":"Fairtlough","year":"2002"},{"key":"10.1016\/j.jal.2011.12.002_br0240","series-title":"Reasoning about Knowledge","author":"Fagin","year":"1995"},{"key":"10.1016\/j.jal.2011.12.002_br0250","doi-asserted-by":"crossref","unstructured":"L. Floridi, semantic information and the network theory of account, Synthese, forthcoming, doi:10.1007\/s11229-010-9821-4.","DOI":"10.1007\/s11229-010-9821-4"},{"key":"10.1016\/j.jal.2011.12.002_br0260","unstructured":"L. Floridi, The Philosophy of Information, Oxford University Press, Oxford."},{"key":"10.1016\/j.jal.2011.12.002_br0270","doi-asserted-by":"crossref","first-page":"393","DOI":"10.1093\/mind\/104.414.393","article-title":"Telling and trusting: reductionism and anti-reductionism in the epistemology of testimony","volume":"104","author":"Fricker","year":"1995","journal-title":"Mind and Society"},{"key":"10.1016\/j.jal.2011.12.002_br0280","first-page":"159","article-title":"A context-based logic for distributed knowledge representation and reasoning","volume":"1688","author":"Ghidini","year":"1999","journal-title":"Lecture Notes in Artificial Intelligence"},{"key":"10.1016\/j.jal.2011.12.002_br0290","unstructured":"F. Giunchiglia, L. Serafini, E. Giunchiglia, M. Frixione, Non-omniscient belief as context-based reasoning, in: International Joint Conferences in Artificial Intelligence, 1993, pp. 548\u2013554."},{"key":"10.1016\/j.jal.2011.12.002_br0300","article-title":"Local models semantics, or contextual reasoning=locality+compatibility","volume":"127","author":"Giunchiglia","year":"1997","journal-title":"Artificial Intelligence"},{"key":"10.1016\/j.jal.2011.12.002_br0310","series-title":"Knowledge in a Social World","author":"Goldman","year":"1999"},{"key":"10.1016\/j.jal.2011.12.002_br0320","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1111\/1467-9213.00057","article-title":"What is testimony?","volume":"47","author":"Graham","year":"1997","journal-title":"Philosophical Quarterly"},{"issue":"1","key":"10.1016\/j.jal.2011.12.002_br0330","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1111\/0029-4624.00205","article-title":"Transferring knowledge","volume":"34","author":"Graham","year":"2000","journal-title":"Nous"},{"issue":"3","key":"10.1016\/j.jal.2011.12.002_br0340","doi-asserted-by":"crossref","first-page":"549","DOI":"10.1145\/79147.79161","article-title":"Knowledge and common knowledge in a distributed environment","volume":"37","author":"Halpern","year":"1990","journal-title":"Journal of the ACM"},{"key":"10.1016\/j.jal.2011.12.002_br0350","doi-asserted-by":"crossref","first-page":"693","DOI":"10.2307\/2027007","article-title":"The role of trust in knowledge","volume":"88","author":"Hardwig","year":"1991","journal-title":"The Journal of Philosophy"},{"key":"10.1016\/j.jal.2011.12.002_br0360","series-title":"NorMAS 2008","first-page":"143","article-title":"Prolegomena for a logic of trust and reputation","author":"Herzig","year":"2008"},{"issue":"1","key":"10.1016\/j.jal.2011.12.002_br0370","doi-asserted-by":"crossref","first-page":"214","DOI":"10.1093\/jigpal\/jzp077","article-title":"A logic of trust and reputation","volume":"18","author":"Herzig","year":"2010","journal-title":"Logic Journal of the IGPL"},{"key":"10.1016\/j.jal.2011.12.002_br0380","series-title":"An Introduction to the Logic of the Notions","author":"Hintikka","year":"1962"},{"key":"10.1016\/j.jal.2011.12.002_br0390","series-title":"LORI\u02bc09: Proceedings of the 2nd International Conference on Logic, Rationality and Interaction","first-page":"161","article-title":"Dynamic testimonial logic","volume":"vol. 5834","author":"Holliday","year":"2009"},{"key":"10.1016\/j.jal.2011.12.002_br0400","series-title":"Proceedings of the 8th International Conference on Electronic Commerce","first-page":"259","article-title":"An ontology of trust. Formal semantics and transitivity","volume":"vol. 156","author":"Huang","year":"2006"},{"key":"10.1016\/j.jal.2011.12.002_br0410","doi-asserted-by":"crossref","first-page":"55","DOI":"10.2307\/2564672","article-title":"Second-hand moral knowledge","volume":"96","author":"Jones","year":"1999","journal-title":"The Journal of Philosophy"},{"issue":"4","key":"10.1016\/j.jal.2011.12.002_br0420","doi-asserted-by":"crossref","DOI":"10.2307\/2269016","article-title":"On the interpretation of intuitionistic number theory","volume":"10","author":"Kleene","year":"1945","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/j.jal.2011.12.002_br0430","series-title":"From Frege to G\u00f6del: A Source Book in Mathematical Logic 1879\u20131931","first-page":"414","article-title":"On the principle of excluded middle","author":"Kolmogorov","year":"1967"},{"issue":"1","key":"10.1016\/j.jal.2011.12.002_br0440","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1145\/1753171.1753193","article-title":"Formal definitions and complexity results for trust relations and trust domains fit for TTPs, the web of trust, PKIs, and ID-based cryptography","volume":"41","author":"Kramer","year":"2010","journal-title":"ACM SIGACT News"},{"key":"10.1016\/j.jal.2011.12.002_br0450","series-title":"Learning from Words. Testimony as a Source of Knowledge","author":"Lackey","year":"2008"},{"issue":"1","key":"10.1016\/j.jal.2011.12.002_br0460","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/S0004-3702(03)00063-8","article-title":"Belief, information acquisition, and trust in multi-agent systems \u2013 A modal logic formulation","volume":"149","author":"Liau","year":"2003","journal-title":"Artificial Intelligence"},{"key":"10.1016\/j.jal.2011.12.002_br0470","series-title":"Proceedings of the 12th International Workshop on Computational Logic in Multi-Agent Systems (CLIMA XII)","first-page":"58","article-title":"A modal framework for relating belief and signed information","volume":"vol. 6814","author":"Lorini","year":"2011"},{"key":"10.1016\/j.jal.2011.12.002_br0480","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/j.entcs.2007.03.024","article-title":"A uniform framework for security and trust modeling and analysis with crypto-CCS","volume":"186","author":"Martinelli","year":"2007","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"10.1016\/j.jal.2011.12.002_br0490","series-title":"Intuitionistic Type Theory","author":"Martin-L\u00f6f","year":"1984"},{"key":"10.1016\/j.jal.2011.12.002_br0500","first-page":"127","article-title":"An intuitionistic theory of types","author":"Martin-L\u00f6f","year":"1998"},{"key":"10.1016\/j.jal.2011.12.002_br0510","unstructured":"J. McCarthy, Notes on formalizing context, in: Proceedings of the 13th Joint Conference on Artificial Intelligence (IJCAI-93), 1993."},{"key":"10.1016\/j.jal.2011.12.002_br0520","series-title":"Trust in Cyber-Societies","first-page":"27","article-title":"The meanings of trust","volume":"vol. 2246","author":"McKnight","year":"2001"},{"key":"10.1016\/j.jal.2011.12.002_br0530","unstructured":"M. Mendler, V. de Paiva, Constructive CK for contexts, in: Proceedings of the First Workshop on Context Representation and Reasoning \u2013 CONTEXT05, Stanford, 2005."},{"key":"10.1016\/j.jal.2011.12.002_br0540","series-title":"Epistemic Logic for AI and Computer Science","author":"Meyer","year":"1995"},{"key":"10.1016\/j.jal.2011.12.002_br0550","unstructured":"T. Murphy, Modal types for mobile code, PhD thesis, CMU-CS-08-126, School of Computer Science, Carnegie-Mellon University, Pittsburgh, PA, 2008."},{"key":"10.1016\/j.jal.2011.12.002_br0560","series-title":"Proceedings of the 19th Annual Symposium on Logic in Computer Science (LICS\u02bc04)","first-page":"286","article-title":"A symmetric modal lambda calculus for distributed computing","author":"Murphy","year":"2004"},{"issue":"3","key":"10.1016\/j.jal.2011.12.002_br0570","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1352582.1352591","article-title":"Contextual modal type theory","volume":"9","author":"Nanevski","year":"2008","journal-title":"ACM Transactions on Computational Logic"},{"key":"10.1016\/j.jal.2011.12.002_br0580","first-page":"100","article-title":"Proof theory for distributed knowledge","volume":"5056","author":"Negri","year":"2008","journal-title":"Lecture Notes in Artificial Intelligence"},{"key":"10.1016\/j.jal.2011.12.002_br0590","article-title":"Programming in Martin-L\u00f6f Type Theory. An Introduction","volume":"vol. 7","author":"Nordstr\u00f6m","year":"1990"},{"key":"10.1016\/j.jal.2011.12.002_br0600","series-title":"Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science","first-page":"221","article-title":"Intensionality, extensionality, and proof irrelevance in modal type theory","author":"Pfenning","year":"2001"},{"key":"10.1016\/j.jal.2011.12.002_br0610","doi-asserted-by":"crossref","first-page":"511","DOI":"10.1017\/S0960129501003322","article-title":"A judgemental reconstruction of modal logic","volume":"11","author":"Pfenning","year":"2001","journal-title":"Mathematical Structures in Computer Science"},{"key":"10.1016\/j.jal.2011.12.002_br0620","article-title":"Information and Knowledge","volume":"vol. 10","author":"Primiero","year":"2008"},{"key":"10.1016\/j.jal.2011.12.002_br0630","series-title":"Proceedings of the First International Workshop on Logic-Based Interpretation of Context: Modelling and Applications","first-page":"33","article-title":"A constructive modal semantics for contextual verification","volume":"vol. 550","author":"Primiero","year":"2009"},{"key":"10.1016\/j.jal.2011.12.002_br0640","series-title":"Acts of Knowledge: History, Philosophy and Logic","first-page":"207","article-title":"Epistemic modalities","volume":"vol. 9","author":"Primiero","year":"2009"},{"key":"10.1016\/j.jal.2011.12.002_br0650","unstructured":"G. Primiero, A contextual type theory with judgemental modalities for reasoning from open assumptions, Logique & Analyse 220 (2012), forthcoming."},{"key":"10.1016\/j.jal.2011.12.002_br0660","unstructured":"G. Primiero, A multi-modal type-theory and its procedural semantics for safe distributed programming, Paper presented at Intuitionistic Modal Logic and Applications Workshop, CLMPS Affiliated, Nancy, 2011, Manuscript."},{"key":"10.1016\/j.jal.2011.12.002_br0670","series-title":"Type-Theoretical Grammar","author":"Ranta","year":"1994"},{"issue":"3","key":"10.1016\/j.jal.2011.12.002_br0680","doi-asserted-by":"crossref","first-page":"413","DOI":"10.1093\/logcom\/12.3.413","article-title":"Engineering executable agents using multi-context systems","volume":"12","author":"Sabater","year":"2002","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/j.jal.2011.12.002_br0690","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1007\/BF00485442","article-title":"Justification, autonomy, sociality","volume":"73","author":"Schmitt","year":"1987","journal-title":"Synthese"},{"key":"10.1016\/j.jal.2011.12.002_br0700","doi-asserted-by":"crossref","unstructured":"C. Sierra, J. Debenham, An information-based model for trust, in: Proceedings of the Fourth International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS 2005, ACM, New York, NY, USA, pp. 497\u2013504.","DOI":"10.1145\/1082473.1082549"},{"key":"10.1016\/j.jal.2011.12.002_br0710","article-title":"Lectures on the Curry\u2013Howard Isomorphism","volume":"vol. 149","author":"S\u00f8rensen","year":"2006"},{"issue":"2","key":"10.1016\/j.jal.2011.12.002_br0720","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1007\/s11023-010-9201-3","article-title":"Modelling trust in artificial agents, a first step toward the analysis of e-trust","volume":"20","author":"Taddeo","year":"2010","journal-title":"Minds and Machines"},{"issue":"4","key":"10.1016\/j.jal.2011.12.002_br0730","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1080\/02691728.2010.521863","article-title":"An information-based solution for the puzzle of testimony and trust","volume":"24","author":"Taddeo","year":"2010","journal-title":"Social Epistemology"},{"key":"10.1016\/j.jal.2011.12.002_br0740","series-title":"Proceedings of the Information Security Conference","first-page":"482","article-title":"A formal definition for trust in distributed systems","volume":"vol. 3650","author":"Xiu","year":"2005"},{"key":"10.1016\/j.jal.2011.12.002_br0750","series-title":"The Community of Knowledge","author":"Welbourne","year":"1993"},{"issue":"2","key":"10.1016\/j.jal.2011.12.002_br0760","doi-asserted-by":"crossref","first-page":"42","DOI":"10.4304\/jcp.1.2.42-53","article-title":"General methodology for analysis and modeling of trust relationships in distributed computing","volume":"1","author":"Zhao","year":"2006","journal-title":"Journal of Computers"}],"container-title":["Journal of Applied Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1570868311000668?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1570868311000668?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2018,11,27]],"date-time":"2018-11-27T14:32:31Z","timestamp":1543329151000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1570868311000668"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,3]]},"references-count":76,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2012,3]]}},"alternative-id":["S1570868311000668"],"URL":"https:\/\/doi.org\/10.1016\/j.jal.2011.12.002","relation":{},"ISSN":["1570-8683"],"issn-type":[{"value":"1570-8683","type":"print"}],"subject":[],"published":{"date-parts":[[2012,3]]}}}