Get quick answers to your questions about the article from our AI researcher chatbot
{'id': 'https://openalex.org/W1987693120', 'doi': 'https://doi.org/10.1002/cpe.598', 'title': 'Hoare logic for Java in Isabelle/HOL', 'display_name': 'Hoare logic for Java in Isabelle/HOL', 'publication_year': 2001, 'publication_date': '2001-11-01', 'ids': {'openalex': 'https://openalex.org/W1987693120', 'doi': 'https://doi.org/10.1002/cpe.598', 'mag': '1987693120'}, 'language': 'en', 'primary_location': {'is_oa': False, 'landing_page_url': 'https://doi.org/10.1002/cpe.598', 'pdf_url': None, 'source': {'id': 'https://openalex.org/S11065456', 'display_name': 'Concurrency and Computation Practice and Experience', 'issn_l': '1532-0626', 'issn': ['1532-0626', '1532-0634'], 'is_oa': False, 'is_in_doaj': False, 'is_core': True, 'host_organization': 'https://openalex.org/P4310320595', 'host_organization_name': 'Wiley', 'host_organization_lineage': ['https://openalex.org/P4310320595'], 'host_organization_lineage_names': ['Wiley'], 'type': 'journal'}, 'license': None, 'license_id': None, 'version': None, 'is_accepted': False, 'is_published': False}, 'type': 'article', 'type_crossref': 'journal-article', 'indexed_in': ['crossref'], 'open_access': {'is_oa': False, 'oa_status': 'closed', 'oa_url': None, 'any_repository_has_fulltext': False}, 'authorships': [{'author_position': 'first', 'author': {'id': 'https://openalex.org/A5050598471', 'display_name': 'David von Oheimb', 'orcid': None}, 'institutions': [{'id': 'https://openalex.org/I62916508', 'display_name': 'Technical University of Munich', 'ror': 'https://ror.org/02kkvpp62', 'country_code': 'DE', 'type': 'education', 'lineage': ['https://openalex.org/I62916508']}], 'countries': ['DE'], 'is_corresponding': True, 'raw_author_name': 'David von Oheimb', 'raw_affiliation_strings': ['Institut für Informatik, Technische Universität München, D-80290, München, Germany#TAB#'], 'affiliations': [{'raw_affiliation_string': 'Institut für Informatik, Technische Universität München, D-80290, München, Germany#TAB#', 'institution_ids': ['https://openalex.org/I62916508']}]}], 'countries_distinct_count': 1, 'institutions_distinct_count': 1, 'corresponding_author_ids': ['https://openalex.org/A5050598471'], 'corresponding_institution_ids': ['https://openalex.org/I62916508'], 'apc_list': {'value': 4740, 'currency': 'USD', 'value_usd': 4740, 'provenance': 'doaj'}, 'apc_paid': None, 'fwci': 10.985, 'has_fulltext': False, 'cited_by_count': 91, 'citation_normalized_percentile': {'value': 0.970142, 'is_in_top_1_percent': False, 'is_in_top_10_percent': True}, 'cited_by_percentile_year': {'min': 95, 'max': 96}, 'biblio': {'volume': '13', 'issue': '13', 'first_page': '1173', 'last_page': '1214'}, 'is_retracted': False, 'is_paratext': False, 'primary_topic': {'id': 'https://openalex.org/T10126', 'display_name': 'Program Analysis and Verification Techniques', 'score': 0.9999, 'subfield': {'id': 'https://openalex.org/subfields/1702', 'display_name': 'Artificial Intelligence'}, 'field': {'id': 'https://openalex.org/fields/17', 'display_name': 'Computer Science'}, 'domain': {'id': 'https://openalex.org/domains/3', 'display_name': 'Physical Sciences'}}, 'topics': [{'id': 'https://openalex.org/T10126', 'display_name': 'Program Analysis and Verification Techniques', 'score': 0.9999, 'subfield': {'id': 'https://openalex.org/subfields/1702', 'display_name': 'Artificial Intelligence'}, 'field': {'id': 'https://openalex.org/fields/17', 'display_name': 'Computer Science'}, 'domain': {'id': 'https://openalex.org/domains/3', 'display_name': 'Physical Sciences'}}, {'id': 'https://openalex.org/T10142', 'display_name': 'Formal Methods in Software Verification and Control', 'score': 0.9984, 'subfield': {'id': 'https://openalex.org/subfields/1703', 'display_name': 'Computational Theory and Mathematics'}, 'field': {'id': 'https://openalex.org/fields/17', 'display_name': 'Computer Science'}, 'domain': {'id': 'https://openalex.org/domains/3', 'display_name': 'Physical Sciences'}}, {'id': 'https://openalex.org/T11010', 'display_name': 'Logic Programming and Knowledge Representation', 'score': 0.993, 'subfield': {'id': 'https://openalex.org/subfields/1702', 'display_name': 'Artificial Intelligence'}, 'field': {'id': 'https://openalex.org/fields/17', 'display_name': 'Computer Science'}, 'domain': {'id': 'https://openalex.org/domains/3', 'display_name': 'Physical Sciences'}}], 'keywords': [{'id': 'https://openalex.org/keywords/hol', 'display_name': 'HOL', 'score': 0.8775881}, {'id': 'https://openalex.org/keywords/hoare-logic', 'display_name': 'Hoare logic', 'score': 0.83570534}, {'id': 'https://openalex.org/keywords/soundness', 'display_name': 'Soundness', 'score': 0.6315164}, {'id': 'https://openalex.org/keywords/separation-logic', 'display_name': 'Separation logic', 'score': 0.5931873}, {'id': 'https://openalex.org/keywords/modal-logics', 'display_name': 'Modal Logics', 'score': 0.507169}, {'id': 'https://openalex.org/keywords/proof-assistant', 'display_name': 'Proof assistant', 'score': 0.4682632}, {'id': 'https://openalex.org/keywords/type-safety', 'display_name': 'Type safety', 'score': 0.44913542}, {'id': 'https://openalex.org/keywords/completeness', 'display_name': 'Completeness (order theory)', 'score': 0.44667384}, {'id': 'https://openalex.org/keywords/predicate-transformer-semantics', 'display_name': 'Predicate transformer semantics', 'score': 0.42597923}], 'concepts': [{'id': 'https://openalex.org/C17435882', 'wikidata': 'https://www.wikidata.org/wiki/Q17030435', 'display_name': 'HOL', 'level': 2, 'score': 0.8775881}, {'id': 'https://openalex.org/C104949639', 'wikidata': 'https://www.wikidata.org/wiki/Q1375924', 'display_name': 'Hoare logic', 'level': 3, 'score': 0.83570534}, {'id': 'https://openalex.org/C199360897', 'wikidata': 'https://www.wikidata.org/wiki/Q9143', 'display_name': 'Programming language', 'level': 1, 'score': 0.748469}, {'id': 'https://openalex.org/C41008148', 'wikidata': 'https://www.wikidata.org/wiki/Q21198', 'display_name': 'Computer science', 'level': 0, 'score': 0.73360413}, {'id': 'https://openalex.org/C39920170', 'wikidata': 'https://www.wikidata.org/wiki/Q693083', 'display_name': 'Soundness', 'level': 2, 'score': 0.6315164}, {'id': 'https://openalex.org/C55439883', 'wikidata': 'https://www.wikidata.org/wiki/Q360812', 'display_name': 'Correctness', 'level': 2, 'score': 0.6282366}, {'id': 'https://openalex.org/C173856430', 'wikidata': 'https://www.wikidata.org/wiki/Q3257964', 'display_name': 'Separation logic', 'level': 2, 'score': 0.5931873}, {'id': 'https://openalex.org/C168773036', 'wikidata': 'https://www.wikidata.org/wiki/Q264164', 'display_name': 'Recursion (computer science)', 'level': 2, 'score': 0.5320626}, {'id': 'https://openalex.org/C108710211', 'wikidata': 'https://www.wikidata.org/wiki/Q11538', 'display_name': 'Mathematical proof', 'level': 2, 'score': 0.52946746}, {'id': 'https://openalex.org/C548217200', 'wikidata': 'https://www.wikidata.org/wiki/Q251', 'display_name': 'Java', 'level': 2, 'score': 0.52674836}, {'id': 'https://openalex.org/C203265346', 'wikidata': 'https://www.wikidata.org/wiki/Q11387554', 'display_name': 'Proof assistant', 'level': 3, 'score': 0.4682632}, {'id': 'https://openalex.org/C206880738', 'wikidata': 'https://www.wikidata.org/wiki/Q431667', 'display_name': 'Automated theorem proving', 'level': 2, 'score': 0.45925185}, {'id': 'https://openalex.org/C44779574', 'wikidata': 'https://www.wikidata.org/wiki/Q736866', 'display_name': 'Type safety', 'level': 2, 'score': 0.44913542}, {'id': 'https://openalex.org/C17231256', 'wikidata': 'https://www.wikidata.org/wiki/Q5156540', 'display_name': 'Completeness (order theory)', 'level': 2, 'score': 0.44667384}, {'id': 'https://openalex.org/C30128091', 'wikidata': 'https://www.wikidata.org/wiki/Q291929', 'display_name': 'Predicate transformer semantics', 'level': 4, 'score': 0.42597923}, {'id': 'https://openalex.org/C80444323', 'wikidata': 'https://www.wikidata.org/wiki/Q2878974', 'display_name': 'Theoretical computer science', 'level': 1, 'score': 0.3784921}, {'id': 'https://openalex.org/C184337299', 'wikidata': 'https://www.wikidata.org/wiki/Q1437428', 'display_name': 'Semantics (computer science)', 'level': 2, 'score': 0.27946365}, {'id': 'https://openalex.org/C156325763', 'wikidata': 'https://www.wikidata.org/wiki/Q1930895', 'display_name': 'Operational semantics', 'level': 3, 'score': 0.24796185}, {'id': 'https://openalex.org/C33923547', 'wikidata': 'https://www.wikidata.org/wiki/Q395', 'display_name': 'Mathematics', 'level': 0, 'score': 0.21700305}, {'id': 'https://openalex.org/C134306372', 'wikidata': 'https://www.wikidata.org/wiki/Q7754', 'display_name': 'Mathematical analysis', 'level': 1, 'score': 0.0}, {'id': 'https://openalex.org/C2524010', 'wikidata': 'https://www.wikidata.org/wiki/Q8087', 'display_name': 'Geometry', 'level': 1, 'score': 0.0}], 'mesh': [], 'locations_count': 1, 'locations': [{'is_oa': False, 'landing_page_url': 'https://doi.org/10.1002/cpe.598', 'pdf_url': None, 'source': {'id': 'https://openalex.org/S11065456', 'display_name': 'Concurrency and Computation Practice and Experience', 'issn_l': '1532-0626', 'issn': ['1532-0626', '1532-0634'], 'is_oa': False, 'is_in_doaj': False, 'is_core': True, 'host_organization': 'https://openalex.org/P4310320595', 'host_organization_name': 'Wiley', 'host_organization_lineage': ['https://openalex.org/P4310320595'], 'host_organization_lineage_names': ['Wiley'], 'type': 'journal'}, 'license': None, 'license_id': None, 'version': None, 'is_accepted': False, 'is_published': False}], 'best_oa_location': None, 'sustainable_development_goals': [], 'grants': [], 'datasets': [], 'versions': [], 'referenced_works_count': 42, 'referenced_works': ['https://openalex.org/W10365329', 'https://openalex.org/W1485193184', 'https://openalex.org/W1498523273', 'https://openalex.org/W1512952371', 'https://openalex.org/W1521083034', 'https://openalex.org/W1533730123', 'https://openalex.org/W1544646281', 'https://openalex.org/W1553537175', 'https://openalex.org/W1569794958', 'https://openalex.org/W1573258001', 'https://openalex.org/W1584721038', 'https://openalex.org/W1586167239', 'https://openalex.org/W1588394470', 'https://openalex.org/W1644882639', 'https://openalex.org/W1772687864', 'https://openalex.org/W1864194708', 'https://openalex.org/W1887681675', 'https://openalex.org/W191371315', 'https://openalex.org/W1918806322', 'https://openalex.org/W1996404651', 'https://openalex.org/W2028904812', 'https://openalex.org/W2032396207', 'https://openalex.org/W2057835515', 'https://openalex.org/W2075350371', 'https://openalex.org/W2094160561', 'https://openalex.org/W2096601022', 'https://openalex.org/W2097185397', 'https://openalex.org/W2107283383', 'https://openalex.org/W2111619838', 'https://openalex.org/W2122291521', 'https://openalex.org/W2127382014', 'https://openalex.org/W2150728514', 'https://openalex.org/W2159484187', 'https://openalex.org/W2165121897', 'https://openalex.org/W2169051420', 'https://openalex.org/W2170898576', 'https://openalex.org/W2561675875', 'https://openalex.org/W2612719351', 'https://openalex.org/W2987907651', 'https://openalex.org/W3146075203', 'https://openalex.org/W4234528212', 'https://openalex.org/W4256124958'], 'related_works': ['https://openalex.org/W4318145497', 'https://openalex.org/W4256587698', 'https://openalex.org/W2963446106', 'https://openalex.org/W2927405667', 'https://openalex.org/W2096553703', 'https://openalex.org/W2018603276', 'https://openalex.org/W2015096460', 'https://openalex.org/W1987693120', 'https://openalex.org/W1864574667', 'https://openalex.org/W1509296872'], 'abstract_inverted_index': {'Abstract': [0], 'This': [1, 162], 'article': [2], 'presents': [3], 'a': [4, 8, 84, 111, 132, 142], 'Hoare‐style': [5], 'calculus': [6], 'for': [7, 72, 115, 136], 'substantial': [9], 'subset': [10], 'of': [11, 43, 55, 86, 94, 102, 107, 124, 129], 'Java': [12, 17, 56], 'Card,': [13], 'which': [14], 'we': [15], 'call': [16], '$^{\\ell': [18, 57], 'ight}$': [19, 58], '.': [20], 'In': [21], 'particular,': [22], 'the': [23, 69, 87, 100, 122, 125, 157, 174], 'language': [24, 75], 'includes': [25], 'side‐effecting': [26, 117], 'expressions,': [27], 'mutual': [28, 137], 'recursion,': [29], 'dynamic': [30], 'method': [31], 'binding,': [32], 'full': [33], 'exception': [34], 'handling,': [35], 'and': [36, 119, 131, 150], 'static': [37], 'class': [38], 'initialization.': [39], 'The': [40, 80, 92], 'Hoare': [41], 'logic': [42, 71], 'partial': [44], 'correctness': [45], 'is': [46, 68, 77], 'proved': [47], 'not': [48, 164], 'only': [49, 165], 'sound': [50], '(w.r.t.': [51], 'our': [52], 'operational': [53], 'semantics': [54], ',': [59], 'described': [60], 'in': [61, 173], 'detail': [62], 'elsewhere)': [63], 'but': [64, 144, 168], 'even': [65], 'complete.': [66, 79], 'It': [67], 'first': [70], 'an': [73], 'object‐oriented': [74], 'that': [76], 'provably': [78], 'completeness': [81], 'proof': [82, 93], 'uses': [83], 'refinement': [85], 'Most': [88], 'General': [89], 'Formula': [90], 'approach.': [91], 'soundness': [95], 'gives': [96, 170], 'new': [97, 112], 'insights': [98], 'into': [99], 'role': [101], 'type': [103], 'safety.': [104], 'Further': [105], 'by‐products': [106], 'this': [108], 'work': [109], 'are': [110], 'general': [113], 'methodology': [114], 'handling': [116], 'expressions': [118], 'their': [120], 'results,': [121], 'discovery': [123], 'strongest': [126], 'possible': [127], 'rule': [128, 135], 'consequence,': [130], 'flexible': [133], 'Call': [134], 'recursion.': [138], 'We': [139], 'also': [140, 169], 'give': [141], 'small': [143], 'non‐trivial': [145], 'application': [146], 'example.': [147], 'All': [148], 'definitions': [149], 'proofs': [151], 'have': [152], 'been': [153], 'done': [154], 'formally': [155], 'with': [156], 'interactive': [158], 'theorem': [159], 'prover': [160], 'Isabelle/HOL.': [161], 'guarantees': [163], 'rigorous': [166], 'definitions,': [167], 'maximal': [171], 'confidence': [172], 'results': [175], 'obtained.': [176], 'Copyright': [177], '©': [178], '2001': [179], 'John': [180], 'Wiley': [181], '&': [182], 'Sons,': [183], 'Ltd.': [184]}, 'cited_by_api_url': 'https://api.openalex.org/works?filter=cites:W1987693120', 'counts_by_year': [{'year': 2022, 'cited_by_count': 1}, {'year': 2021, 'cited_by_count': 2}, {'year': 2019, 'cited_by_count': 3}, {'year': 2018, 'cited_by_count': 3}, {'year': 2017, 'cited_by_count': 2}, {'year': 2016, 'cited_by_count': 1}, {'year': 2015, 'cited_by_count': 4}, {'year': 2014, 'cited_by_count': 8}, {'year': 2013, 'cited_by_count': 4}, {'year': 2012, 'cited_by_count': 4}], 'updated_date': '2024-08-31T15:38:36.122219', 'created_date': '2016-06-24'}