A Direct Algorithm for Type Inference in the Rank-2 Fragment of the Second-Order lambda-Calculus. - A. J. Kfoury; J. B. Wells (LISP and Functional Programming, 1994)

Typability and Type-Checking in the Second-Order lambda-Calculus are Equivalent and Undecidable - J. B. Wells (LICS, 1994)

New Notions of Reduction and Non-Semantic Proofs of beta-Strong Normalization in Typed lambda-Calculi - A. J. Kfoury; J. B. Wells (LICS, 1995)

Strongly Typed Flow-Directed Representation Transformations. - Allyn Dimock; Robert Muller; Franklyn A. Turbak; J. B. Wells (ICFP, 1997)

A Typed Intermediate Language for Flow-Directed Compilation. - J. B. Wells; Allyn Dimock; Robert Muller; Franklyn A. Turbak (TAPSOFT, 1997)

Calculi of Generalized beta-Reduction and Explicit Substitutions: The Type-Free and Simply Typed Versions. - Fairouz Kamareddine; Alejandro Ríos 001; J. B. Wells (J. Funct. Log. Program., 1998)

Relating Typability and Expressiveness in Finite-Rank Intersection Type Systems (Extended Abstract). - Assaf J. Kfoury; Harry G. Mairson; Franklyn A. Turbak; J. B. Wells (ICFP, 1999)

Principality and Decidable Type Inference for Finite-Rank Intersection Types. - A. J. Kfoury; J. B. Wells (POPL, 1999)

Typability and Type Checking in System F are Equivalent and Undecidable. - J. B. Wells (Ann. Pure Appl. Log., 1999)

Equational Reasoning for Linking with First-Class Primitive Modules. - J. B. Wells; René Vestergaard (ESOP, 2000)

Introduction: Workshop on Intersection Types and Related Systems (ITRS'00). - J. B. Wells (ICALP Satellite Workshops, 2000)

Program Representation Size in an Intermediate Language with Intersection and Union Types. - Allyn Dimock; Ian Westmacott; Robert Muller; Franklyn A. Turbak; J. B. Wells; Jeffrey Considine (Types in Compilation, 2000)

Functioning without Closure: Type-Safe Customized Function Representations for Standard ML. - Allyn Dimock; Ian Westmacott; Robert Muller; Franklyn A. Turbak; J. B. Wells (ICFP, 2001)

Cycle Therapy: A Prescription for Fold and Unfold on Regular Trees. - Franklyn A. Turbak; J. B. Wells (PPDP, 2001)

Cut rules and explicit substitutions. - René Vestergaard; J. B. Wells (Math. Struct. Comput. Sci., 2001)

Fully Automatic Adaptation of Software Components Based on Semantic Specifications. - Christian Haack; Brian Howard 001; Allen Stoughton; Joe B. Wells (AMAST, 2002)

Branching Types. - Joe B. Wells; Christian Haack (ESOP, 2002)

The Essence of Principal Typings. - J. B. Wells (ICALP, 2002)

Implementing Compositional Analysis Using Intersection Types With Expansion Variables. - Assaf J. Kfoury; Geoffrey Washburn; Joe B. Wells (ITRS, 2002)

A calculus with polymorphic and polyvariant flow types. - J. B. Wells; Allyn Dimock; Robert Muller; Franklyn A. Turbak (J. Funct. Program., 2002)

Diagrams for Meaning Preservation. - J. B. Wells; Detlef Plump; Fairouz Kamareddine (RTA, 2003)

MathLang: Experience-driven Development of a New Mathematical Language. - Fairouz Kamareddine; Manuel Maarek; J. B. Wells (MKM Symposium, 2003)

System E: Expansion Variables for Flexible Typing with Linear and Non-linear Types and Intersection Types. - Sébastien Carlier; Jeff Polakow; J. B. Wells; A. J. Kfoury (ESOP, 2004)

Call-by-Value Mixin Modules: Reduction Semantics, Side Effects, Types. - Tom Hirschowitz; Xavier Leroy; J. B. Wells (ESOP, 2004)

PolyA: True Type Polymorphism for Mobile Ambients. - Torben Amtoft; Henning Makholm; J. B. Wells (IFIP TCS, 2004)

Graph-Based Proof Counting and Enumeration with Applications for Program Fragment Synthesis. - J. B. Wells; Boris Yakobowski (LOPSTR, 2004)

Flexible Encoding of Mathematics on the Computer. - Fairouz Kamareddine; Manuel Maarek; J. B. Wells (MKM, 2004)

Type inference with expansion variables and intersection types in system E and an exact correspondence with beta-reduction. - Sébastien Carlier; J. B. Wells (PPDP, 2004)

Expansion: the Crucial Mechanism for Type Inference with Intersection Types: A Survey and Explanation. - Sébastien Carlier; J. B. Wells (ITRS, 2004)

Type error slicing in implicitly typed higher-order languages. - Christian Haack; Joe B. Wells (Sci. Comput. Program., 2004)

Principality and type inference for intersection types using expansion variables. - A. J. Kfoury; J. B. Wells (Theor. Comput. Sci., 2004)

Instant Polymorphic Type Systems for Mobile Process Calculi: Just Add Reduction Rules and Close. - Henning Makholm; J. B. Wells (ESOP, 2005)

Type inference, principal typings, and let-polymorphism for first-class mixin modules. - Henning Makholm; J. B. Wells (ICFP, 2005)

Toward an Object-Oriented Structure for Mathematical Text. - Fairouz Kamareddine; Manuel Maarek; J. B. Wells (MKM, 2005)

Restoring Natural Language as a Computerised Mathematics Input Method. - Fairouz Kamareddine; Robert Lamar; Manuel Maarek; J. B. Wells (Calculemus/MKM, 2007)

Narrative Structure of Mathematical Texts. - Fairouz Kamareddine; Manuel Maarek; Krzysztof Retel; J. B. Wells (Calculemus/MKM, 2007)

Computerizing Mathematical Text with MathLang. - Fairouz Kamareddine; J. B. Wells (LSFA, 2007)

A Complete Realisability Semantics for Intersection Types and Arbitrary Expansion Variables. - Fairouz Kamareddine; Karim Nour; Vincent Rahli; J. B. Wells (ICTAC, 2008)

MathLang Translation to Isabelle Syntax. - Robert Lamar; Fairouz Kamareddine; J. B. Wells (Calculemus/MKM, 2009)

Compilation of extended recursion in call-by-value functional languages. - Tom Hirschowitz; Xavier Leroy; J. B. Wells (High. Order Symb. Comput., 2009)

Expressiveness of Generic Process Shape Types. - Jan Jakubuv; J. B. Wells (TGC, 2010)

Expansion for Universal Quantifiers. - Sergueï Lenglet; Joe B. Wells (ESOP, 2012)

The Algebra of Expansion. - Sébastien Carlier; J. B. Wells (Fundam. Informaticae, 2012)

On Realisability Semantics for Intersection Types with Expansion Variables. - Fairouz Kamareddine; Karim Nour; Vincent Rahli; J. B. Wells (Fundam. Informaticae, 2012)

Reducibility Proofs in the λ-Calculus. - Fairouz Kamareddine; Vincent Rahli; J. B. Wells (Fundam. Informaticae, 2012)

Skalpel: A Type Error Slicer for Standard ML. - Vincent Rahli; Joe B. Wells; John Pirie; Fairouz Kamareddine (LSFA, 2014)

Computerising Mathematical Text. - Fairouz Kamareddine; Joe B. Wells; Christoph Zengler; Henk Barendregt (Computational Logic, 2014)

Automath Type Inclusion in Barendregt's Cube. - Fairouz Kamareddine; Joe B. Wells; Daniel Lima Ventura (CSR, 2015)

Bridging Curry and Church's typing style. - Fairouz Kamareddine; Jonathan P. Seldin; J. B. Wells (J. Appl. Log., 2016)

Skalpel: A constraint-based type error slicer for Standard ML. - Vincent Rahli; Joe B. Wells; John Pirie; Fairouz Kamareddine (J. Symb. Comput., 2017)

What Does This Notation Mean Anyway? - David Feller; Joe B. Wells; Fairouz Kamareddine; Sébastien Carlier (CoRR, 2018)

BNF-Style Notation as It Is Actually Used. - Dee Quinlan; Joe B. Wells; Fairouz Kamareddine (CICM, 2019)

Proof-Carrying Plans. - Christopher Schwaab; Ekaterina Komendantskaya; Alasdair Hill; Frantisek Farka; Ronald P. A. Petrick; Joe B. Wells; Kevin Hammond (PADL, 2019)

Adding an Abstraction Barrier to ZF Set Theory. - Ciarán Dunne; J. B. Wells; Fairouz Kamareddine (CICM, 2020)

Generating Custom Set Theories with Non-set Structured Objects. - Ciarán Dunne; J. B. Wells; Fairouz Kamareddine (CICM, 2021)

Isabelle/HOL/GST: A Formal Proof Environment for Generalized Set Theories. - Ciarán Dunne; J. B. Wells (CICM, 2022)

Towards Semantic Markup of Mathematical Documents via User Interaction. - Luka Vrecar; Joe B. Wells; Fairouz Kamareddine (CICM, 2024)

Intersection Types via Finite-Set Declarations. - Fairouz Kamareddine; Joe B. Wells (WoLLIC, 2024)