{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,4]],"date-time":"2023-09-04T23:17:16Z","timestamp":1693869436203},"reference-count":20,"publisher":"Open Publishing Association","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electron. Proc. Theor. Comput. Sci.","EPTCS"],"DOI":"10.4204\/eptcs.191.12","type":"journal-article","created":{"date-parts":[[2015,9,9]],"date-time":"2015-09-09T13:14:56Z","timestamp":1441804496000},"page":"132-142","source":"Crossref","is-referenced-by-count":4,"title":["A Type-Directed Negation Elimination"],"prefix":"10.4204","volume":"191","author":[{"given":"Etienne","family":"Lozes","sequence":"first","affiliation":[{"name":"ENS Cachan, CNRS"}]}],"member":"2720","published-online":{"date-parts":[[2015,9,9]]},"reference":[{"issue":"2","key":"AxelssonLS07","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-3(2:7)2007","article-title":"The Complexity of Model Checking Higher-Order Fixpoint Logic","volume":"3","author":"Axelsson","year":"2007","journal-title":"Logical Methods in Computer Science"},{"key":"BroadbentCHS13","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1145\/2500365.2500589","article-title":"C-SHORe: a collapsible approach to higher-order verification","volume-title":"ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013","author":"Broadbent","year":"2013"},{"key":"Bruse14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-662-44522-8_10","article-title":"Alternating Parity Krivine Automata","volume-title":"Mathematical Foundations of Computer Science 2014","volume":"8634","author":"Bruse","year":"2014"},{"key":"Cachat03","doi-asserted-by":"publisher","first-page":"556","DOI":"10.1007\/3-540-45061-0_45","article-title":"Higher Order Pushdown Automata, the Caucal Hierarchy of Graphs and Parity Games","volume-title":"Automata, Languages and Programming, 30th International Colloquium, ICALP 2003, Eindhoven, The Netherlands, June 30 - July 4, 2003. Proceedings","author":"Cachat","year":"2003"},{"key":"CarayolS12","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1109\/LICS.2012.73","article-title":"Collapsible Pushdown Automata and Labeled Recursion Schemes: Equivalence, Safety and Effective Selection","volume-title":"LICS","author":"Carayol","year":"2012"},{"issue":"2","key":"Damm198295","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0304-3975(82)90009-3","article-title":"The IO- and OI-hierarchies","volume":"20","author":"Damm","year":"1982","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"DawarGK04","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1145\/976706.976710","article-title":"Inflationary fixed points in modal logic","volume":"5","author":"Dawar","year":"2004","journal-title":"ACM Trans. Comput. Log."},{"key":"Filliatre-hash","series-title":"ML '06","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/1159876.1159880","article-title":"Type-safe Modular Hash-consing","volume-title":"Proceedings of the 2006 Workshop on ML","author":"Filli\u00e2tre","year":"2006"},{"key":"FujimaIK13","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-319-03542-0_2","article-title":"Practical Alternating Parity Tree Automata Model Checking of Higher-Order Recursion Schemes","volume-title":"Programming Languages and Systems - 11th Asian Symposium, APLAS 2013, Melbourne, VIC, Australia, December 9-11, 2013. Proceedings","author":"Fujima","year":"2013"},{"key":"Gonthier92thegeometry","series-title":"POPL '92","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1145\/143165.143172","article-title":"The Geometry of Optimal Lambda Reduction","volume-title":"Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Gonthier","year":"1992"},{"key":"Goubault-hash","first-page":"222","article-title":"Implementing Functional Languages with Fast Equality Sets and Maps: an Exercise in Hash Cons","volume-title":"Journ\u00e9es Francophones des Langages Applicatifs (JFLA'93)","author":"Goubault","year":"1993"},{"key":"HagueMOS08","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1109\/LICS.2008.34","article-title":"Collapsible Pushdown Automata and Recursion Schemes","volume-title":"Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA","author":"Hague","year":"2008"},{"key":"Lamping90","series-title":"POPL '90","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1145\/96709.96711","article-title":"An Algorithm for Optimal Lambda Calculus Reduction","volume-title":"Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Lamping","year":"1990"},{"key":"LangeL14","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-662-44602-7_8","article-title":"Capturing Bisimulation-Invariant Complexity Classes with Higher-Order Modal Fixpoint Logic","volume-title":"Theoretical Computer Science - 8th IFIP TC 1\/WG 2.2 International Conference, TCS 2014, Rome, Italy, September 1-3, 2014. Proceedings","author":"Lange","year":"2014"},{"key":"phdlaurent","volume-title":"Etude de la polarisation en logique","author":"Laurent","year":"2002"},{"key":"Mackie98","series-title":"ICFP '98","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1145\/289423.289434","article-title":"YALE: Yet Another Lambda Evaluator Based on Interaction Nets","volume-title":"Proceedings of the Third ACM SIGPLAN International Conference on Functional Programming","author":"Mackie","year":"1998"},{"key":"Maslov76","first-page":"38","article-title":"Multilevel stack automata","volume":"12","author":"Maslov.","year":"1976","journal-title":"Problems of Information Transmission"},{"key":"SalvatiW14","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1016\/j.ic.2014.07.012","article-title":"Krivine machines and higher-order schemes","volume":"239","author":"Salvati","year":"2014","journal-title":"Inf. Comput."},{"key":"TeraoK14","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-319-12736-1_19","article-title":"A ZDD-Based Efficient Higher-Order Model Checking Algorithm","volume-title":"Programming Languages and Systems - 12th Asian Symposium, APLAS 2014, Singapore, November 17-19, 2014, Proceedings","author":"Terao","year":"2014"},{"key":"ViswanathanV04","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/978-3-540-28644-8_33","article-title":"A Higher Order Modal Fixed Point Logic","volume-title":"CONCUR","volume":"3170","author":"Viswanathan","year":"2004"}],"container-title":["Electronic Proceedings in Theoretical Computer Science"],"original-title":[],"language":"en","deposited":{"date-parts":[[2015,9,18]],"date-time":"2015-09-18T10:25:23Z","timestamp":1442571923000},"score":1,"resource":{"primary":{"URL":"http:\/\/arxiv.org\/abs\/1509.03020"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,9,9]]},"references-count":20,"URL":"https:\/\/doi.org\/10.4204\/eptcs.191.12","relation":{},"ISSN":["2075-2180"],"issn-type":[{"value":"2075-2180","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,9,9]]}}}