publications:
- title: "Binders unbound"
  author:
  - name: "Stephanie Weirich"
    link: "https://researchr.org/alias/stephanie-weirich"
  - name: "Brent A. Yorgey"
    link: "https://researchr.org/alias/brent-a.-yorgey"
  - name: "Tim Sheard"
    link: "https://researchr.org/alias/tim-sheard"
  year: "2011"
  doi: "http://doi.acm.org/10.1145/2034773.2034818"
  links:
    doi: "http://doi.acm.org/10.1145/2034773.2034818"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/WeirichYS11"
  researchr: "https://researchr.org/publication/WeirichYS11"
  cites: 0
  citedby: 0
  pages: "333-345"
  booktitle: "Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011"
  editor:
  - name: "Manuel M. T. Chakravarty"
    link: "https://researchr.org/alias/manuel-m.-t.-chakravarty"
  - name: "Zhenjiang Hu"
    link: "https://researchr.org/alias/zhenjiang-hu"
  - name: "Olivier Danvy"
    link: "https://www.yale-nus.edu.sg/about/faculty/olivier-danvy/"
  publisher: "ACM"
  isbn: "978-1-4503-0865-6"
  kind: "inproceedings"
  key: "WeirichYS11"
- title: "Substitution: A Formal Methods Case Study Using Monads and Transformations"
  author:
  - name: "Françoise Bellegarde"
    link: "https://researchr.org/alias/fran%C3%A7oise-bellegarde"
  - name: "James Hook"
    link: "https://researchr.org/alias/james-hook"
  year: "1994"
  tags:
  - "case study"
  - "transformation"
  researchr: "https://researchr.org/publication/BellegardeH94"
  cites: 0
  citedby: 0
  journal: "Science of Computer Programming"
  volume: "23"
  number: "2-3"
  pages: "287-311"
  kind: "article"
  key: "BellegardeH94"
- title: "A fresh look at programming with names and binders"
  author:
  - name: "Nicolas Pouillard"
    link: "https://researchr.org/alias/nicolas-pouillard"
  - name: "François Pottier"
    link: "https://researchr.org/alias/fran%C3%A7ois-pottier"
  year: "2010"
  doi: "http://doi.acm.org/10.1145/1863543.1863575"
  links:
    doi: "http://doi.acm.org/10.1145/1863543.1863575"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/PouillardP10"
  tags:
  - "programming"
  researchr: "https://researchr.org/publication/PouillardP10"
  cites: 0
  citedby: 0
  pages: "217-228"
  booktitle: "Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010"
  editor:
  - name: "Paul Hudak"
    link: "https://researchr.org/alias/paul-hudak"
  - name: "Stephanie Weirich"
    link: "https://researchr.org/alias/stephanie-weirich"
  publisher: "ACM"
  isbn: "978-1-60558-794-3"
  kind: "inproceedings"
  key: "PouillardP10"
- title: "A Theory of Name Resolution"
  author:
  - name: "Pierre Néron"
    link: "https://researchr.org/profile/pierrejeanmichelneron/publications"
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  - name: "Eelco Visser"
    link: "http://eelcovisser.org"
  - name: "Guido Wachsmuth"
    link: "https://www.linkedin.com/in/guidowachsmuth/"
  year: "2015"
  doi: "http://dx.doi.org/10.1007/978-3-662-46669-8_9"
  abstract: "We describe a language-independent theory for name binding and resolution, suitable for programming languages with complex scoping rules including both lexical scoping and modules. We formulate name resolution as a two-stage problem. First a language-independent scope graph is constructed using language-specific rules from an abstract syntax tree. Then references in the scope graph are resolved to corresponding declarations using a language-independent resolution process. We introduce a resolution calculus as a concise, declarative, and languageindependent specification of name resolution. We develop a resolution algorithm that is sound and complete with respect to the calculus. Based on the resolution calculus we develop language-independent definitions of α-equivalence and rename refactoring. We illustrate the approach using a small example language with modules. In addition, we show how our approach provides a model for a range of name binding patterns in existing languages."
  links:
    doi: "http://dx.doi.org/10.1007/978-3-662-46669-8_9"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/esop/NeronTVW15"
    technicalreport: "https://researchr.org/publication/TUD-SERG-2015-001"
  researchr: "https://researchr.org/publication/NeronTVW15"
  cites: 0
  citedby: 0
  pages: "205-231"
  booktitle: "Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings"
  editor:
  - name: "Jan Vitek"
    link: "https://researchr.org/alias/jan-vitek"
  volume: "9032"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-662-46668-1"
  kind: "inproceedings"
  key: "NeronTVW15"
- title: "A New Approach to Abstract Syntax with Variable Binding"
  author:
  - name: "Murdoch Gabbay"
    link: "https://researchr.org/alias/murdoch-gabbay"
  - name: "Andrew M. Pitts"
    link: "https://researchr.org/alias/andrew-m.-pitts"
  year: "2002"
  doi: "http://link.springer.de/link/service/journals/00165/bibs/2013003/20130341.htm"
  links:
    doi: "http://link.springer.de/link/service/journals/00165/bibs/2013003/20130341.htm"
  tags:
  - "abstract syntax"
  - "variable binding"
  - "systematic-approach"
  researchr: "https://researchr.org/publication/GabbayP02"
  cites: 0
  citedby: 0
  journal: "Formal Asp. Comput."
  volume: "13"
  number: "3-5"
  pages: "341-363"
  kind: "article"
  key: "GabbayP02"
- title: "Binding Structures as an Abstract Data Type"
  author:
  - name: "Wilmer Ricciotti"
    link: "https://researchr.org/alias/wilmer-ricciotti"
  year: "2015"
  doi: "http://dx.doi.org/10.1007/978-3-662-46669-8_31"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-662-46669-8_31"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/esop/Ricciotti15"
  researchr: "https://researchr.org/publication/Ricciotti15"
  cites: 0
  citedby: 0
  pages: "762-786"
  booktitle: "Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings"
  editor:
  - name: "Jan Vitek"
    link: "https://researchr.org/alias/jan-vitek"
  volume: "9032"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-662-46668-1"
  kind: "inproceedings"
  key: "Ricciotti15"
- title: "Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem"
  author:
  - name: "N. G. de Bruijn"
    link: "https://researchr.org/alias/n.-g.-de-bruijn"
  year: "1972"
  researchr: "https://researchr.org/publication/deBruijn72"
  cites: 0
  citedby: 0
  journal: "Indagationes Mathematicae"
  volume: "34"
  number: "5"
  pages: "381-392"
  kind: "article"
  key: "deBruijn72"
- title: "Higher-Order Abstract Syntax"
  author:
  - name: "Frank Pfenning"
    link: "http://www.cs.cmu.edu/~fp/"
  - name: "Conal Elliott"
    link: "http://conal.net/"
  year: "1988"
  doi: "https://doi.org/10.1145/960116.54010"
  links:
    doi: "https://doi.org/10.1145/960116.54010"
  tags:
  - "abstract syntax"
  researchr: "https://researchr.org/publication/PfenningE88"
  cites: 0
  citedby: 0
  pages: "199-208"
  booktitle: "PLDI"
  kind: "inproceedings"
  key: "PfenningE88"
- title: "Parametric higher-order abstract syntax for mechanized semantics"
  author:
  - name: "Adam J. Chlipala"
    link: "http://adam.chlipala.net/"
  year: "2008"
  doi: "http://doi.acm.org/10.1145/1411204.1411226"
  links:
    doi: "http://doi.acm.org/10.1145/1411204.1411226"
  tags:
  - "semantics"
  - "abstract syntax"
  researchr: "https://researchr.org/publication/Chlipala08"
  cites: 0
  citedby: 0
  pages: "143-156"
  booktitle: "Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, ICFP 2008, Victoria, BC, Canada, September 20-28, 2008"
  editor:
  - name: "James Hook"
    link: "https://researchr.org/alias/james-hook"
  - name: "Peter Thiemann"
    link: "http://www.informatik.uni-freiburg.de/~thiemann/"
  publisher: "ACM"
  isbn: "978-1-59593-919-7"
  kind: "inproceedings"
  key: "Chlipala08"
- title: "The Locally Nameless Representation"
  author:
  - name: "Arthur Charguéraud"
    link: "https://researchr.org/alias/arthur-chargu%C3%A9raud"
  year: "2012"
  doi: "http://dx.doi.org/10.1007/s10817-011-9225-2"
  links:
    doi: "http://dx.doi.org/10.1007/s10817-011-9225-2"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jar/Chargueraud12"
  researchr: "https://researchr.org/publication/Chargueraud12"
  cites: 0
  citedby: 0
  journal: "Journal of Automated Reasoning"
  volume: "49"
  number: "3"
  pages: "363-408"
  kind: "article"
  key: "Chargueraud12"
- title: "Names for free: polymorphic views of names and binders"
  author:
  - name: "Jean-Philippe Bernardy"
    link: "https://researchr.org/alias/jean-philippe-bernardy"
  - name: "Nicolas Pouillard"
    link: "https://researchr.org/alias/nicolas-pouillard"
  year: "2013"
  doi: "http://doi.acm.org/10.1145/2503778.2503780"
  links:
    doi: "http://doi.acm.org/10.1145/2503778.2503780"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/haskell/BernardyP13"
  researchr: "https://researchr.org/publication/BernardyP13"
  cites: 0
  citedby: 0
  pages: "13-24"
  booktitle: "Proceedings of the 2013 ACM SIGPLAN Symposium on Haskell, Boston, MA, USA, September 23-24, 2013"
  editor:
  - name: "Chung-chieh Shan"
    link: "https://researchr.org/alias/chung-chieh-shan"
  publisher: "ACM"
  isbn: "978-1-4503-2383-3"
  kind: "inproceedings"
  key: "BernardyP13"
- title: "Pure Type Systems Formalized"
  author:
  - name: "James McKinna"
    link: "https://researchr.org/alias/james-mckinna"
  - name: "Robert Pollack"
    link: "https://researchr.org/alias/robert-pollack"
  year: "1993"
  tags:
  - "type system"
  researchr: "https://researchr.org/publication/McKinnaP93"
  cites: 0
  citedby: 0
  pages: "289-305"
  booktitle: "Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA  93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings"
  editor:
  - name: "Marc Bezem"
    link: "http://www.ii.uib.no/~bezem/"
  - name: "Jan Friso Groote"
    link: "http://www.win.tue.nl/~jfg/"
  volume: "664"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "3-540-56517-5"
  kind: "inproceedings"
  key: "McKinnaP93"
- title: "Nameless, painless"
  author:
  - name: "Nicolas Pouillard"
    link: "https://researchr.org/alias/nicolas-pouillard"
  year: "2011"
  doi: "http://doi.acm.org/10.1145/2034773.2034817"
  links:
    doi: "http://doi.acm.org/10.1145/2034773.2034817"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/Pouillard11"
  researchr: "https://researchr.org/publication/Pouillard11"
  cites: 0
  citedby: 0
  pages: "320-332"
  booktitle: "Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011"
  editor:
  - name: "Manuel M. T. Chakravarty"
    link: "https://researchr.org/alias/manuel-m.-t.-chakravarty"
  - name: "Zhenjiang Hu"
    link: "https://researchr.org/alias/zhenjiang-hu"
  - name: "Olivier Danvy"
    link: "https://www.yale-nus.edu.sg/about/faculty/olivier-danvy/"
  publisher: "ACM"
  isbn: "978-1-4503-0865-6"
  kind: "inproceedings"
  key: "Pouillard11"
- title: "Everybody's Got To Be Somewhere"
  author:
  - name: "Conor McBride"
    link: "http://personal.cis.strath.ac.uk/~conor/"
  year: "2018"
  month: "Jul"
  doi: "10.4204/eptcs.275.6"
  links:
    "url": "http://dx.doi.org/10.4204/EPTCS.275.6"
  researchr: "https://researchr.org/publication/McBride2018"
  cites: 0
  citedby: 0
  journal: "Electronic Proceedings in Theoretical Computer Science"
  volume: "275"
  pages: "53-69"
  kind: "article"
  key: "McBride2018"
- title: "Scopes as types"
  author:
  - name: "Hendrik van Antwerpen"
    link: "https://nl.linkedin.com/in/hendrikvanantwerpen"
  - name: "Casper Bach Poulsen"
    link: "http://www.casperbp.net"
  - name: "Arjen Rouvoet"
    link: "https://www.linkedin.com/in/arjen-rouvoet-760347a5/"
  - name: "Eelco Visser"
    link: "http://eelcovisser.org"
  year: "2018"
  doi: "https://doi.org/10.1145/3276484"
  abstract: "Scope graphs are a promising generic framework to model the binding structures of programming languages, bridging formalization and implementation, supporting the definition of type checkers and the automation of type safety proofs. However, previous work on scope graphs has been limited to simple, nominal type systems. In this paper, we show that viewing scopes as types enables us to model the internal structure of types in a range of non-simple type systems (including structural records and generic classes) using the generic representation of scopes. Further, we show that relations between such types can be expressed in terms of generalized scope graph queries. We extend scope graphs with scoped relations and queries. We introduce Statix, a new domain-specific meta-language for the specification of static semantics, based on scope graphs and constraints. We evaluate the scopes as types approach and the Statix design in case studies of the simply-typed lambda calculus with records, System F, and Featherweight Generic Java."
  links:
    doi: "https://doi.org/10.1145/3276484"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/AntwerpenPRV18"
  researchr: "https://researchr.org/publication/AntwerpenPRV18"
  cites: 0
  citedby: 0
  journal: "Proceedings of the ACM on Programming Languages"
  volume: "2"
  number: "OOPSLA"
  kind: "article"
  key: "AntwerpenPRV18"
- title: "FreshML: programming with binders made simple"
  author:
  - name: "Mark R. Shinwell"
    link: "https://researchr.org/alias/mark-r.-shinwell"
  - name: "Andrew M. Pitts"
    link: "https://researchr.org/alias/andrew-m.-pitts"
  - name: "Murdoch Gabbay"
    link: "https://researchr.org/alias/murdoch-gabbay"
  year: "2003"
  doi: "http://doi.acm.org/10.1145/944705.944729"
  links:
    doi: "http://doi.acm.org/10.1145/944705.944729"
  tags:
  - "programming"
  researchr: "https://researchr.org/publication/ShinwellPG03"
  cites: 0
  citedby: 0
  pages: "263-274"
  booktitle: "Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, ICFP 2003, Uppsala, Sweden, August 25-29, 2003"
  editor:
  - name: "Colin Runciman"
    link: "https://researchr.org/alias/colin-runciman"
  - name: "Olin Shivers"
    link: "https://researchr.org/alias/olin-shivers"
  publisher: "ACM"
  isbn: "1-58113-756-7"
  kind: "inproceedings"
  key: "ShinwellPG03"
- title: "Nominal logic, a first order theory of names and binding"
  author:
  - name: "Andrew M. Pitts"
    link: "https://researchr.org/alias/andrew-m.-pitts"
  year: "2003"
  doi: "http://dx.doi.org/10.1016/S0890-5401(03)00138-X"
  links:
    doi: "http://dx.doi.org/10.1016/S0890-5401(03)00138-X"
  tags:
  - "logic"
  researchr: "https://researchr.org/publication/Pitts03"
  cites: 0
  citedby: 0
  journal: "Inf. Comput."
  volume: "186"
  number: "2"
  pages: "165-193"
  kind: "article"
  key: "Pitts03"
- title: "The Spoofax Name Binding Language"
  author:
  - name: "Gabriël Konat"
    link: "http://nl.linkedin.com/in/gabrielkonat"
  - name: "Vlad A. Vergu"
    link: "http://www.linkedin.com/in/vladv"
  - name: "Lennart C. L. Kats"
    link: "http://www.lclnet.nl/"
  - name: "Guido Wachsmuth"
    link: "https://www.linkedin.com/in/guidowachsmuth/"
  - name: "Eelco Visser"
    link: "http://eelcovisser.org"
  year: "2012"
  doi: "https://doi.org/10.1145/2384716.2384748"
  abstract: "In textual software languages, names are used to identify program elements such as variables, methods, and classes. Name analysis algorithms resolve names in order to establish references between definitions and uses of names. In this poster, we present the Spoofax Name Binding Language (NBL), a declarative meta-language for the specification of name binding and scope rules, which departs from the programmatic encodings of name binding provided by regular approaches. NBL aspires to become the universal language for name binding, which can be used next to BNF definitions in reference manuals, as well as serve the generation of implementations."
  links:
    doi: "https://doi.org/10.1145/2384716.2384748"
    "url": "https://doi.org/10.1145/2384716.2384748"
  tags:
  - "C++"
  - "Spoofax"
  researchr: "https://researchr.org/publication/KonatVKWV2012"
  cites: 0
  citedby: 0
  booktitle: "Companion to the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2011, part of SPLASH 2012, Tucson, AR, USA, October 19 - 26, 2012"
  publisher: "ACM"
  kind: "inproceedings"
  key: "KonatVKWV2012"
- title: "Knowing when to ask: sound scheduling of name resolution in type checkers derived from declarative specifications"
  author:
  - name: "Arjen Rouvoet"
    link: "https://www.linkedin.com/in/arjen-rouvoet-760347a5/"
  - name: "Hendrik van Antwerpen"
    link: "https://researchr.org/alias/hendrik-van-antwerpen"
  - name: "Casper Bach Poulsen"
    link: "http://www.casperbp.net"
  - name: "Robbert Krebbers"
    link: "https://researchr.org/alias/robbert-krebbers"
  - name: "Eelco Visser"
    link: "http://eelcovisser.org"
  year: "2020"
  doi: "https://doi.org/10.1145/3428248"
  abstract: "There is a large gap between the specification of type systems and the implementation of their type checkers, which impedes reasoning about the soundness of the type checker with respect to the specification. A vision to close this gap is to automatically obtain type checkers from declarative programming language specifications. This moves the burden of proving correctness from a case-by-case basis for concrete languages to a single correctness proof for the specification language. This vision is obstructed by an aspect common to all programming languages: name resolution. Naming and scoping are pervasive and complex aspects of the static semantics of programming languages. Implementations of type checkers for languages with name binding features such as modules, imports, classes, and inheritance interleave collection of binding information (i.e., declarations, scoping structure, and imports) and querying that information. This requires scheduling those two aspects in such a way that query answers are stable—i.e., they are computed only after all relevant binding structure has been collected. Type checkers for concrete languages accomplish stability using language-specific knowledge about the type system. In this paper we give a language-independent characterization of necessary and sufficient conditions to guarantee stability of name and type queries during type checking in terms of critical edges in an incomplete scope graph. We use critical edges to give a formal small-step operational semantics to a declarative specification language for type systems, that achieves soundness by delaying queries that may depend on missing information. This yields type checkers for the specified languages that are sound by construction—i.e., they schedule queries so that the answers are stable, and only accept programs that are name- and type-correct according to the declarative language specification. We implement this approach, and evaluate it against specifications of a small module and record language, as well as subsets of Java and Scala."
  links:
    doi: "https://doi.org/10.1145/3428248"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/RouvoetAPKV20"
  researchr: "https://researchr.org/publication/RouvoetAPKV20"
  cites: 0
  citedby: 0
  journal: "Proceedings of the ACM on Programming Languages"
  volume: "4"
  number: "OOPSLA"
  kind: "article"
  key: "RouvoetAPKV20"
- title: "A type and scope safe universe of syntaxes with binding: their semantics and proofs"
  author:
  - name: "Guillaume Allais"
    link: "https://researchr.org/alias/guillaume-allais"
  - name: "Robert Atkey"
    link: "https://researchr.org/alias/robert-atkey"
  - name: "James Chapman"
    link: "https://jmchapman.github.io/"
  - name: "Conor McBride"
    link: "http://personal.cis.strath.ac.uk/~conor/"
  - name: "James McKinna"
    link: "https://researchr.org/alias/james-mckinna"
  year: "2018"
  doi: "https://doi.org/10.1145/3236785"
  links:
    doi: "https://doi.org/10.1145/3236785"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/AllaisA0MM18"
  researchr: "https://researchr.org/publication/AllaisA0MM18"
  cites: 0
  citedby: 0
  journal: "Proceedings of the ACM on Programming Languages"
  volume: "2"
  number: "ICFP"
  kind: "article"
  key: "AllaisA0MM18"
- title: "Engineering formal metatheory"
  author:
  - name: "Brian E. Aydemir"
    link: "https://researchr.org/alias/brian-e.-aydemir"
  - name: "Arthur Charguéraud"
    link: "https://researchr.org/alias/arthur-chargu%C3%A9raud"
  - name: "Benjamin C. Pierce"
    link: "http://www.cis.upenn.edu/~bcpierce/"
  - name: "Randy Pollack"
    link: "https://researchr.org/alias/randy-pollack"
  - name: "Stephanie Weirich"
    link: "http://www.cis.upenn.edu/~sweirich/"
  year: "2008"
  doi: "http://doi.acm.org/10.1145/1328438.1328443"
  abstract: "Machine-checked proofs of properties of programming languages have become a critical need, both for increased confidence in large and complex designs and as a foundation for technologies such as proof-carrying code. However, constructing these proofs remains a black art, involving many choices in the formulation of definitions and theorems that make a huge cumulative difference in the difficulty of carrying out large formal developments. The representation and manipulation of terms with variable binding is a key issue. We propose a novel style for formalizing metatheory, combining locally nameless representation of terms and cofinite quantification of free variable names in inductive definitions of relations on terms (typing, reduction, ...). The key technical insight is that our use of cofinite quantification obviates the need for reasoning about equivariance (the fact that free names can be renamed in derivations); in particular, the structural induction principles of relations defined using cofinite quantification are strong enough for metatheoretic reasoning, and need not be explicitly strengthened. Strong inversion principles follow (automatically, in Coq) from the induction principles. Although many of the underlying ingredients of our technique have been used before, their combination here yields a significant improvement over existing methodology, leading to developments that are faithful to informal practice, yet require no external tool support and little infrastructure within the proof assistant. We have carried out several large developments in this style using the Coq proof assistant and have made them publicly available. Our developments include type soundness for and ML (with references, exceptions, datatypes, recursion and patterns) and subject reduction for the Calculus of Constructions. Not only do these developments demonstrate the comprehensiveness of our approach; they have also been optimized for clarity and robustness, making them good templates for future extension. "
  links:
    doi: "http://doi.acm.org/10.1145/1328438.1328443"
  tags:
  - "programming languages"
  - "optimization"
  - "object-oriented programming"
  - "Machanized Metatheory"
  - "proof assistant"
  - "pattern language"
  - "type soundness"
  - "exceptions"
  - "Coq"
  - "variable binding"
  - "language engineering"
  - "Cofinite quantification"
  - "principles"
  - "little language"
  - "C++"
  - "metatheory"
  - "programming"
  - "subject-oriented programming"
  - "Syntactic type soundness"
  - "program optimization"
  - "systematic-approach"
  - "feature-oriented programming"
  - "Locally nameless"
  researchr: "https://researchr.org/publication/AydemirCPPW08"
  cites: 0
  citedby: 0
  pages: "3-15"
  booktitle: "Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008"
  editor:
  - name: "George C. Necula"
    link: "https://researchr.org/alias/george-c.-necula"
  - name: "Philip Wadler"
    link: "http://homepages.inf.ed.ac.uk/wadler/"
  publisher: "ACM"
  isbn: "978-1-59593-689-9"
  kind: "inproceedings"
  key: "AydemirCPPW08"
- title: "An Overview of C-alpha-ml"
  author:
  - name: "François Pottier"
    link: "https://researchr.org/alias/fran%C3%A7ois-pottier"
  year: "2006"
  doi: "http://dx.doi.org/10.1016/j.entcs.2005.11.039"
  abstract: "Cαml is a tool that turns a so-called “binding specification” into an Objective Caml compilation unit. A binding specification resembles an algebraic data type declaration, but also includes information about names and binding. Cαml is meant to help writers of interpreters, compilers, or other programs-that-manipulate-programs deal with α-conversion in a safe and concise style. This paper presents an overview of Cαml's binding specification language and of the code that Cαml produces."
  links:
    doi: "http://dx.doi.org/10.1016/j.entcs.2005.11.039"
  tags:
  - "C++"
  researchr: "https://researchr.org/publication/Pottier06"
  cites: 0
  citedby: 0
  journal: "Electronic Notes in Theoretical Computer Science"
  volume: "148"
  number: "2"
  pages: "27-52"
  kind: "article"
  key: "Pottier06"
- title: "Nominal unification"
  author:
  - name: "Christian Urban"
    link: "https://researchr.org/alias/christian-urban"
  - name: "Andrew M. Pitts"
    link: "https://researchr.org/alias/andrew-m.-pitts"
  - name: "Murdoch Gabbay"
    link: "https://researchr.org/alias/murdoch-gabbay"
  year: "2004"
  doi: "http://dx.doi.org/10.1016/j.tcs.2004.06.016"
  links:
    doi: "http://dx.doi.org/10.1016/j.tcs.2004.06.016"
  researchr: "https://researchr.org/publication/UrbanPG04"
  cites: 0
  citedby: 0
  journal: "Theoretical Computer Science"
  volume: "323"
  number: "1-3"
  pages: "473-497"
  kind: "article"
  key: "UrbanPG04"
- title: "Namely, Painless: A unifying approach to safe programming with first-order syntax with binders. (Une approche unifiante pour programmer sûrement avec de la syntaxe du premier ordre contenant des lieurs)"
  author:
  - name: "Nicolas Pouillard"
    link: "https://researchr.org/alias/nicolas-pouillard"
  year: "2012"
  doi: "https://tel.archives-ouvertes.fr/tel-00759059"
  links:
    doi: "https://tel.archives-ouvertes.fr/tel-00759059"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/phd/hal/Pouillard12"
  researchr: "https://researchr.org/publication/hal-3916"
  cites: 0
  citedby: 0
  school: "Paris Diderot University, France"
  kind: "phdthesis"
  key: "hal-3916"