{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:45:14Z","timestamp":1772163914344,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":47,"publisher":"ACM","license":[{"start":{"date-parts":[[2007,10,1]],"date-time":"2007-10-01T00:00:00Z","timestamp":1191196800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2007,10]]},"DOI":"10.1145\/1291151.1291155","type":"proceedings-article","created":{"date-parts":[[2007,10,14]],"date-time":"2007-10-14T08:51:38Z","timestamp":1192351898000},"page":"1-12","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":42,"title":["Ott"],"prefix":"10.1145","author":[{"given":"Peter","family":"Sewell","sequence":"first","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}]},{"given":"Francesco Zappa","family":"Nardelli","sequence":"additional","affiliation":[{"name":"INRIA, Rocquencourt, France"}]},{"given":"Scott","family":"Owens","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}]},{"given":"Gilles","family":"Peskine","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}]},{"given":"Thomas","family":"Ridge","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}]},{"given":"Susmit","family":"Sarkar","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}]},{"given":"Rok","family":"Strni\u0161a","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2007,10]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"AFP. The archive of formal proofs. http:\/\/afp.sf.net.  AFP. The archive of formal proofs. http:\/\/afp.sf.net."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328443"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_4"},{"key":"e_1_3_2_1_4_1","first-page":"46","volume-title":"Proc. Int. Workshop on Logical Frameworks and Meta-Languages: Theory and Practice","author":"Berghofer S.","year":"2006","unstructured":"S. Berghofer and C. Urban . A head-to-head comparison of de Bruijn indices and names . In Proc. Int. Workshop on Logical Frameworks and Meta-Languages: Theory and Practice , pages 46 -- 59 , 2006 . S. Berghofer and C. Urban. A head-to-head comparison of de Bruijn indices and names. In Proc. Int. Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, pages 46--59, 2006."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_31"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/64135.65005"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/646481.691428"},{"key":"e_1_3_2_1_8_1","unstructured":"A. Chargu\u00e9raud. Annotated bibliography for formalization of lambda-calculus and type theory. http:\/\/fling-l.seas.upenn.edu\/~plclub\/cgi-bin\/poplmark\/index.php?title=Annotated_Bibliography July 2006.  A. Chargu\u00e9raud. Annotated bibliography for formalization of lambda-calculus and type theory. http:\/\/fling-l.seas.upenn.edu\/~plclub\/cgi-bin\/poplmark\/index.php?title=Annotated_Bibliography July 2006."},{"key":"e_1_3_2_1_9_1","first-page":"269","volume-title":"Proc. ICLP, LNCS 3132","author":"Cheney J.","year":"2004","unstructured":"J. Cheney and C. Urban . Alpha-Prolog: A logic programming language with names, binding and alpha-equivalence . In Proc. ICLP, LNCS 3132 , pages 269 -- 283 , 2004 . J. Cheney and C. Urban. Alpha-Prolog: A logic programming language with names, binding and alpha-equivalence. In Proc. ICLP, LNCS 3132, pages 269--283, 2004."},{"key":"e_1_3_2_1_10_1","unstructured":"Coq. The Coq proof assistant v.8.0. http:\/\/coq.inria.fr\/.  Coq. The Coq proof assistant v.8.0. http:\/\/coq.inria.fr\/."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11737414_4"},{"key":"e_1_3_2_1_12_1","volume-title":"Chapter 10","author":"Findler R. B.","year":"2007","unstructured":"R. B. Findler and J. Matthews . Revised 5:92 report on the algorithmic language Scheme , Chapter 10 , Formal Semantics , Jan. 2007 . R. B. Findler and J. Matthews. Revised 5:92 report on the algorithmic language Scheme, Chapter 10, Formal Semantics, Jan. 2007."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/646731.703841"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/646521.759249"},{"key":"e_1_3_2_1_15_1","unstructured":"HOL. The HOL 4 system Kananaskis-3 release. http:\/\/hol.sourceforge.net\/.  HOL. The HOL 4 system Kananaskis-3 release. http:\/\/hol.sourceforge.net\/."},{"key":"e_1_3_2_1_16_1","unstructured":"Isabelle. Isabelle 2005. http:\/\/isabelle.in.tum.de\/.  Isabelle. Isabelle 2005. http:\/\/isabelle.in.tum.de\/."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/216261.216269"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146809.1146811"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/151257.151260"},{"key":"e_1_3_2_1_21_1","volume-title":"Symposium on Trends in Functional Programming","author":"Lakin M. R.","year":"2007","unstructured":"M. R. Lakin and A. M. Pitts . A metalanguage for structural operational semantics . In Symposium on Trends in Functional Programming , 2007 . M. R. Lakin and A. M. Pitts. A metalanguage for structural operational semantics. In Symposium on Trends in Functional Programming, 2007."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190245"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/64135.65006"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800001933"},{"key":"e_1_3_2_1_25_1","volume-title":"Oct.","author":"Leroy X.","year":"2005","unstructured":"X. Leroy The Objective Caml system release 3.09 documentation and user's manual , Oct. 2005 . X. Leroy et al. The Objective Caml system release 3.09 documentation and user's manual, Oct. 2005."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004550"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-25979-4_21"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/800235.807067"},{"key":"e_1_3_2_1_29_1","volume-title":"The Definition of Standard ML","author":"Milner R.","year":"1990","unstructured":"R. Milner , M. Tofte , and R. Harper . The Definition of Standard ML . MIT Press , 1990 . R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. MIT Press, 1990."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/646061.676146"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/645393.651894"},{"key":"e_1_3_2_1_32_1","first-page":"36","volume-title":"Proceedings of the First Isabelle Users Workshop","author":"Owens C.","year":"1995","unstructured":"C. Owens . Coding binding and substitution explicitly in Isabelle . In Proceedings of the First Isabelle Users Workshop , pages 36 -- 52 , 1995 . C. Owens. Coding binding and substitution explicitly in Isabelle. In Proceedings of the First Isabelle Users Workshop, pages 36--52, 1995."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159815"},{"key":"e_1_3_2_1_34_1","volume-title":"The Revised Report. CUP","author":"Peyton Jones S.","year":"2003","unstructured":"S. Peyton Jones , editor. Haskell 98 Language and Libraries . The Revised Report. CUP , 2003 . S. Peyton Jones, editor. Haskell 98 Language and Libraries. The Revised Report. CUP, 2003."},{"key":"e_1_3_2_1_35_1","volume-title":"MIT Press","author":"Pierce B. C.","year":"2002","unstructured":"B. C. Pierce . Types and Programming Languages . MIT Press , 2002 . B. C. Pierce. Types and Programming Languages. MIT Press, 2002."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.11.039"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/800020.808247"},{"key":"e_1_3_2_1_38_1","volume-title":"Defects in the revised definition of Standard ML. Technical report","author":"Rossberg A.","year":"2001","unstructured":"A. Rossberg . Defects in the revised definition of Standard ML. Technical report , Saarland University , 2001 . Updated 2007\/01\/22. A. Rossberg. Defects in the revised definition of Standard ML. Technical report, Saarland University, 2001. Updated 2007\/01\/22."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"crossref","unstructured":"P. Sewell and F. Zappa Nardelli. Ott 2007. http:\/\/www.cl.cam.ac.uk\/users\/pes20\/ott\/.  P. Sewell and F. Zappa Nardelli. Ott 2007. http:\/\/www.cl.cam.ac.uk\/users\/pes20\/ott\/.","DOI":"10.1145\/1291151.1291155"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/944705.944729"},{"key":"e_1_3_2_1_42_1","volume-title":"Formal Language Description Languages for Computer Programming. North Holland","author":"Strachey C.","year":"1966","unstructured":"C. Strachey . Towards a formal semantics . In Formal Language Description Languages for Computer Programming. North Holland , 1966 . C. Strachey. Towards a formal semantics. In Formal Language Description Languages for Computer Programming. North Holland, 1966."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297027.1297064"},{"key":"e_1_3_2_1_44_1","first-page":"43","volume-title":"TPHOLs, LNCS 780","author":"Syme D.","year":"1993","unstructured":"D. Syme . Reasoning with the formal definition of Standard ML in HOL. In TPHOLs, LNCS 780 , pages 43 -- 59 , 1993 . D. Syme. Reasoning with the formal definition of Standard ML in HOL. In TPHOLs, LNCS 780, pages 43--59, 1993."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/646056.758568"},{"key":"e_1_3_2_1_46_1","volume-title":"Concise concrete syntax","author":"Tse S.","year":"2006","unstructured":"S. Tse and S. Zdancewic . Concise concrete syntax , 2006 . Submitted . http:\/\/www.cis.upenn.edu\/~stse\/javac. S. Tse and S. Zdancewic. Concise concrete syntax, 2006. Submitted. http:\/\/www.cis.upenn.edu\/~stse\/javac."},{"key":"e_1_3_2_1_47_1","unstructured":"Twelf. Twelf 1.5. http:\/\/www.cs.cmu.edu\/~twelf\/.  Twelf. Twelf 1.5. http:\/\/www.cs.cmu.edu\/~twelf\/."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.5555\/2392200.2392220"},{"key":"e_1_3_2_1_49_1","volume-title":"Univ. of Pennsylvania","author":"VanInwegen M.","year":"1996","unstructured":"M. VanInwegen . The Machine-Assisted Proof of Programming Language Properties. PhD thesis , Univ. of Pennsylvania , 1996 . Computer and Information Science Tech Report MS-CIS-96-31. M. VanInwegen. The Machine-Assisted Proof of Programming Language Properties. PhD thesis, Univ. of Pennsylvania, 1996. Computer and Information Science Tech Report MS-CIS-96-31."}],"event":{"name":"ICFP07: ACM SIGPLAN International Conference on Functional Programming","location":"Freiburg Germany","acronym":"ICFP07","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"]},"container-title":["Proceedings of the 12th ACM SIGPLAN international conference on Functional programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1291151.1291155","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1291151.1291155","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:52:25Z","timestamp":1750243945000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1291151.1291155"}},"subtitle":["effective tool support for the working semanticist"],"short-title":[],"issued":{"date-parts":[[2007,10]]},"references-count":47,"alternative-id":["10.1145\/1291151.1291155","10.1145\/1291151"],"URL":"https:\/\/doi.org\/10.1145\/1291151.1291155","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1291220.1291155","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2007,10]]},"assertion":[{"value":"2007-10-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}