3 citations · 7 across the 6 of their papers we have counts for
7 papers
Isabelle/HOL/GST: A Formal Proof Environment for Generalized Set Theories
Ciarán Dunne, J. B. Wells
A generalized set theory (GST) is like a standard set theory but also can have non-set structured objects that can contain other structured objects including sets. This paper prese…
Adding an Abstraction Barrier to ZF Set Theory
Ciarán Dunne, J. B. Wells, Fairouz Kamareddine
Much mathematical writing exists that is, explicitly or implicitly, based on set theory, often Zermelo-Fraenkel set theory (ZF) or one of its variants. In ZF, the domain of discour…
What Does This Notation Mean Anyway?
David Feller, Joe B. Wells, Fairouz Kamareddine +1
Following the introduction of BNF notation by Backus for the Algol 60 report and subsequent notational variants, a metalanguage involving formal "grammars" has developed for discus…
Expansion for Universal Quantifiers
Sergueï Lenglet, J. B. Wells
Expansion is an operation on typings (i.e., pairs of typing environments and result types) defined originally in type systems for the lambda-calculus with intersection types in ord…
Proceedings Fifth Workshop on Intersection Types and Related Systems
Elaine Pimentel, Betti Venneri, Joe Wells
This volume contains the proceedings of the Fifth International Workshop on Intersection Types and Related Systems (ITRS 2010). The workshop was held in Edinburgh, Scotland, on Jul…
Realisability Semantics for Intersection Types and Expansion Variables
Fairouz Kamareddine, Karim Nour, Vincent Rahli +1
Expansion was invented at the end of the 1970s for calculating principal typings for -terms in type systems with intersection types. Expansion variables (E-variables) were inven…