HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

From urelements to Computation

Abstract : Around 1922-1938, a new permutation model of set theory was defined. The permutation model served as a counterexample in the first proof of independence of the Axiom of Choice from the other axioms of Zermelo-Fraenkel set theory. Almost a century later, a model introduced as part of a proof in abstract mathematics fostered a plethora of research results, ranging from the area of syntax and semantics of programming languages to minimization algorithms and automated verification of systems. Among these results, we find Lawvere-style algebraic syntax with binders, final-coalgebra semantics with resource allocation, and minimization algorithms for mobile systems. These results are also obtained in various different ways, by describing, in terms of category theory, a number of models equivalent to the permutation model.We aim at providing both a brief history of some of these developments, and a mild introduction to the recent research line of “nominal computation theory”, where the essential notion of name is declined in several different ways.
Document type :
Conference papers
Complete list of metadata

Cited literature [42 references]  Display  Hide  Download

Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Thursday, October 12, 2017 - 11:22:05 AM
Last modification on : Tuesday, July 31, 2018 - 4:58:01 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Vincenzo Ciancia. From urelements to Computation. 3rd International Conference on History and Philosophy of Computing (HaPoC), Oct 2015, Pisa, Italy. pp.141-155, ⟨10.1007/978-3-319-47286-7_10⟩. ⟨hal-01615302⟩



Record views


Files downloads