`Travelled to:`

1 × Estonia

1 × Germany

1 × Sweden

1 × The Netherlands

1 × United Kingdom

2 × France

3 × Spain

3 × USA

4 × Italy

`Collaborated with:`

A.J.Kfoury F.A.Turbak H.Makholm ∅ S.Carlier A.Dimock T.Hirschowitz X.Leroy B.Yakobowski R.Vestergaard R.Müller D.Plump F.Kamareddine J.Polakow A.J.Kfoury H.G.Mairson R.Muller I.Westmacott

`Talks about:`

type (19) intersect (4) system (4) reduct (4) infer (4) function (3) princip (3) direct (3) modul (3) rank (3)

## Person: J. B. Wells

### DBLP: Wells:J=_B=

### Contributed to:

### Wrote 19 papers:

- ESOP-2005-MakholmW #calculus #mobile #polymorphism #process #reduction #type system
- Instant Polymorphic Type Systems for Mobile Process Calculi: Just Add Reduction Rules and Close (HM, JBW), pp. 389–407.
- ICFP-2005-MakholmW #mixin #morphism #type inference
- Type inference, principal typings, and let-polymorphism for first-class mixin modules (HM, JBW), pp. 156–167.
- ESOP-2004-CarlierPWK #flexibility #linear #type system
- System E: Expansion Variables for Flexible Typing with Linear and Non-linear Types and Intersection Types (SC, JP, JBW, AJK), pp. 294–309.
- ESOP-2004-HirschowitzLW #call-by #mixin #reduction #semantics
- Call-by-Value Mixin Modules: Reduction Semantics, Side Effects, Types (TH, XL, JBW), pp. 64–78.
- LOPSTR-2004-WellsY #graph #proving #synthesis
- Graph-Based Proof Counting and Enumeration with Applications for Program Fragment Synthesis (JBW, BY), pp. 262–277.
- PPDP-2004-CarlierW #type inference
- Type inference with expansion variables and intersection types in system E and an exact correspondence with β-reduction (SC, JBW), pp. 132–143.
- PPDP-2003-HirschowitzLW #call-by #compilation #functional #recursion
- Compilation of extended recursion in call-by-value functional languages (TH, XL, JBW), pp. 160–171.
- RTA-2003-WellsPK #diagrams
- Diagrams for Meaning Preservation (JBW, DP, FK), pp. 88–106.
- ICALP-2002-Wells
- The Essence of Principal Typings (JBW), pp. 913–925.
- ICFP-2001-DimockWMTW #ml #standard #type safety
- Functioning without Closure: Type-Safe Customized Function Representations for Standard ML (AD, IW, RM, FAT, JBW), pp. 14–25.
- PPDP-2001-TurbakW
- Cycle Therapy: A Prescription for Fold and Unfold on Regular Trees (FAT, JBW), pp. 137–149.
- ESOP-2000-WellsV #equation #reasoning
- Equational Reasoning for Linking with First-Class Primitive Modules (JBW, RV), pp. 412–428.
- ICFP-1999-KfouryMTW #type system
- Relating Typability and Expressiveness in Finite-Rank Intersection Type Systems (AJK, HGM, FAT, JBW), pp. 90–101.
- POPL-1999-KfouryW #decidability #type inference
- Principality and Decidable Type Inference for Finite-Rank Intersection Types (AJK, JBW), pp. 161–174.
- ICFP-1997-DimockMTW #representation
- Strongly Typed Flow-Directed Representation Transformations (AD, RM, FAT, JBW), pp. 11–24.
- LICS-1995-KfouryW #normalisation #proving #reduction #semantics #λ-calculus
- New Notions of Reduction and Non-Semantic Proofs of β-Strong Normalization in Typed λ-Calculi (AJK, JBW), pp. 311–321.
- LFP-1994-KfouryW #algorithm #higher-order #type inference #λ-calculus
- A Direct Algorithm for Type Inference in the Rank-2 Fragment of the Second-Order λ-Calculus (AJK, JBW), pp. 196–207.
- LICS-1994-Wells #decidability #higher-order #λ-calculus
- Typability and Type-Checking in the Second-Order λ-Calculus are Equivalent and Undecidable (JBW), pp. 176–185.
- TAPSOFT-1997-WellsDMT #compilation
- A Typed Intermediate Language for Flow-Directed Compilation (JBW, AD, RM, FAT), pp. 757–771.