FreshML: programming with binders made simple. FreshML extends ML with elegant and practical constructs for declaring and manipulating syntactical data involving statically scoped binding operations. User-declared FreshML datatypes involving binders are concrete, in the sense that values of these types can be deconstructed by matching against patterns naming bound variables explicitly. This may have the computational effect of swapping bound names with freshly generated ones; previous work on FreshML used a complicated static type system inferring information about the ’freshness’ of names for expressions in order to tame this effect. The main contribution of this paper is to show (perhaps surprisingly) that a standard type system without freshness inference, coupled with a conventional treatment of fresh name generation, suffices for FreshML’s crucial correctness property that values of datatypes involving binders are operationally equivalent if and only if they represent a-equivalent pieces of object-level syntax. This is established via a novel denotational semantics. FreshML without static freshness inference is no more impure than ML and experience with it shows that it supports a programming style pleasingly close to informal practice when it comes to dealing with object-level syntax modulo a-equivalence.

This software is also peer reviewed by journal TOMS.

References in zbMATH (referenced in 50 articles )

Showing results 1 to 20 of 50.
Sorted by year (citations)

1 2 3 next

  1. Domínguez, Jesús; Fernández, Maribel: Nominal syntax with atom substitutions (2021)
  2. Aceto, Luca; Fábregas, Ignacio; García-Pérez, Álvaro; Ingólfsdóttir, Anna; Ortega-Mallén, Yolanda: Rule formats for nominal process calculi (2019)
  3. Ayala-Rincón, Mauricio; de Carvalho-Segundo, Washington; Fernández, Maribel; Nantes-Sobrinho, Daniele; Rocha-Oliveira, Ana Cristina: A formalisation of nominal (\alpha)-equivalence with A, C, and AC function symbols (2019)
  4. Miller, Dale: Mechanized metatheory revisited (2019)
  5. Ancona, Davide; Giannini, Paola; Zucca, Elena: Constrained polymorphic types for a calculus with name variables (2018)
  6. Benton, Nick; Hofmann, Martin; Nigam, Vivek: Proof-relevant logical relations for name generation (2018)
  7. Rahli, Vincent; Bickford, Mark: Validating Brouwer’s continuity principle for numbers using named exceptions (2018)
  8. Ayala-Rincón, Mauricio; de Carvalho-Segundo, Washington; Fernández, Maribel; Nantes-Sobrinho, Daniele: A formalisation of nominal (\alpha)-equivalence with A and AC function symbols (2017)
  9. Ferreira, Francisco; Pientka, Brigitte: Programs using syntax with first-class binders (2017)
  10. Ancona, Davide; Giannini, Paola; Zucca, Elena: Incremental rebinding with name polymorphism (2016)
  11. Azevedo de Amorim, Arthur: Binding operators for nominal sets (2016)
  12. Kiselyov, Oleg; Kameyama, Yukiyoshi; Sudo, Yuto: Refined environment classifiers. Type- and scope-safe code generation with mutable cells (2016)
  13. Pitts, Andrew M.; Matthiesen, Justus; Derikx, Jasper: A dependent type theory with abstractable names (2015)
  14. Lösch, Steffen; Pitts, Andrew M.: Denotational semantics with nominal Scott domains (2014)
  15. Clouston, Ranald: Generalised name abstraction for nominal sets (2013)
  16. Savary-Belanger, Olivier; Monnier, Stefan; Pientka, Brigitte: Programming type-safe transformations using higher-order abstract syntax (2013)
  17. Charguéraud, Arthur: The locally nameless representation (2012)
  18. Cheney, James: A dependent nominal type theory (2012)
  19. Kurz, Alexander; Suzuki, Tomoyuki; Tuosto, Emilio: On nominal regular languages with binders (2012)
  20. Calvès, Christophe; Fernández, Maribel: The first-order nominal link (2011)

1 2 3 next