{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T13:26:19Z","timestamp":1730294779306,"version":"3.28.0"},"reference-count":19,"publisher":"IEEE Comput. Soc","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/scam.2002.1134107","type":"proceedings-article","created":{"date-parts":[[2003,6,26]],"date-time":"2003-06-26T01:03:42Z","timestamp":1056589422000},"page":"73-82","source":"Crossref","is-referenced-by-count":1,"title":["Mechanized operational semantics of WSL"],"prefix":"10.1109","author":[{"family":"Xingyuan Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Munro","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Harman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"family":"Lin Hu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","article-title":"Computation and Reasoning: A Type Theory for Computer Science","author":"luo","year":"1994","journal-title":"No 11 in International Series of Monographs on Computer Science"},{"journal-title":"The Implementation of ALF—a Proof Editor Based on Martin-Löf's Monomorphic Type Theory with Explicit Substitution","year":"1994","author":"magnusson","key":"ref11"},{"key":"ref12","article-title":"Programming in Martin-Lof's Type Theory","volume":"7","author":"nordstr\u00f6m","year":"1990","journal-title":"ser The International Series of Monographs on Computer Science"},{"key":"ref13","article-title":"The Coq proof assistant, A tutorial, version 5.10","author":"huet","year":"1995","journal-title":"Technical Report RT-0178"},{"key":"ref14","article-title":"A tutorial on recursive types in Coq","author":"gimenez","year":"1998","journal-title":"Technical Report RT-0221"},{"key":"ref15","article-title":"The Coq proof assistant, reference manual, version 7.0","author":"comes","year":"2001","journal-title":"Technical Report RT-0177"},{"journal-title":"Proving Program Refinements and Transformations","year":"1989","author":"ward","key":"ref16"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/ICSM.1989.65225"},{"key":"ref18","article-title":"Assembler to c migration using the fermat transformation system","author":"ward","year":"1999","journal-title":"IEEE International Conference on Software Maintenance (ICSM'99) (Oxford UK)"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45685-6_22"},{"journal-title":"Introduction to HOL A Theorem Proving Environment for Higher Order Logic","year":"1993","author":"gordon","key":"ref4"},{"key":"ref3","first-page":"2","article-title":"Introduction to the HOL system","author":"gordon","year":"1992","journal-title":"Proceedigns of the International Workshop on the HOL Theorem Proving System and its Applications"},{"key":"ref6","article-title":"Isabelle tutorial and user's manual","author":"paulson","year":"1990","journal-title":"Tech Rep TR-189"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541"},{"key":"ref8","article-title":"User Guide for the PVS Specification and Verification System","author":"owre","year":"1993","journal-title":"Computer Science Laboratory SRI International"},{"key":"ref7","article-title":"A tutorial on specification and verification using PVS","author":"shankar","year":"1993","journal-title":"preliminary draft Csl report SRI International"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/48529.48530"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/359104.359106"},{"journal-title":"Tech Rep ECS-LFCS-92–211","year":"1992","author":"luo","key":"ref9"}],"event":{"name":"Second IEEE International Workshop on Source Code Analysis and Manipulation","acronym":"SCAM-02","location":"Montreal, Que., Canada"},"container-title":["Proceedings. Second IEEE International Workshop on Source Code Analysis and Manipulation"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/8211\/25179\/01134107.pdf?arnumber=1134107","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,3,13]],"date-time":"2017-03-13T16:43:06Z","timestamp":1489423386000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1134107\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":19,"URL":"https:\/\/doi.org\/10.1109\/scam.2002.1134107","relation":{},"subject":[]}}