### Abstract

This entry defines a type class with an operator returning a fresh identifier, given a set of already used identifiers and a preferred identifier. The entry provides a default instantiation for any infinite type, as well as executable instantiations for natural numbers and strings.

### License

BSD License

### Topics

- Computer science/Data structures

### Session Fresh_Identifiers

- Fresh
- Fresh_Nat
- Fresh_String
- Fresh_Infinite

### Used by

- MLSS Decision Procedure
- CoCon: A Confidentiality-Verified Conference Management System
- CoSMed: A confidentiality-verified social media platform
- CoSMeDis: A confidentiality-verified distributed social media platform
- First-Order Terms

## Cite

×

Fresh_Identifiers-AFP

    @article{Fresh_Identifiers-AFP,
      author  = {Andrei Popescu and Thomas Bauereiss},
      title   = {Fresh identifiers},
      journal = {Archive of Formal Proofs},
      month   = {August},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/Fresh_Identifiers.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Aug 18, 2021 : Isabelle2021