{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T08:07:26Z","timestamp":1649146046864},"reference-count":0,"publisher":"Open Publishing Association","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electron. Proc. Theor. Comput. Sci.","EPTCS"],"DOI":"10.4204\/eptcs.192.4","type":"journal-article","created":{"date-parts":[[2015,9,18]],"date-time":"2015-09-18T06:25:30Z","timestamp":1442557530000},"page":"35-51","source":"Crossref","is-referenced-by-count":1,"title":["Fourier Series Formalization in ACL2(r)"],"prefix":"10.4204","volume":"192","author":[{"given":"Cuong K.","family":"Chau","sequence":"first","affiliation":[{"name":"The University of Texas at Austin"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matt","family":"Kaufmann","sequence":"additional","affiliation":[{"name":"The University of Texas at Austin"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"suffix":"Jr.","given":"Warren A.","family":"Hunt","sequence":"additional","affiliation":[{"name":"The University of Texas at Austin"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"2720","published-online":{"date-parts":[[2015,9,18]]},"container-title":["Electronic Proceedings in Theoretical Computer Science"],"original-title":[],"language":"en","deposited":{"date-parts":[[2015,9,23]],"date-time":"2015-09-23T02:38:13Z","timestamp":1442975893000},"score":1,"resource":{"primary":{"URL":"https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/http\/arxiv.org\/abs\/1509.06087"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,9,18]]},"references-count":0,"URL":"https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/https\/doi.org\/10.4204\/eptcs.192.4","relation":{},"ISSN":["2075-2180"],"issn-type":[{"value":"2075-2180","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,9,18]]}}}