Joe B. Wells

Affiliations:
  • Heriot-Watt University, Edinburgh, UK


According to our database1, Joe B. Wells authored at least 56 papers between 1994 and 2022.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2022
Isabelle/HOL/GST: A Formal Proof Environment for Generalized Set Theories.
Proceedings of the Intelligent Computer Mathematics - 15th International Conference, 2022

2021
Generating Custom Set Theories with Non-set Structured Objects.
Proceedings of the Intelligent Computer Mathematics - 14th International Conference, 2021

2020
Adding an Abstraction Barrier to ZF Set Theory.
Proceedings of the Intelligent Computer Mathematics - 13th International Conference, 2020

2019
Proof-Carrying Plans.
Proceedings of the Practical Aspects of Declarative Languages, 2019

BNF-Style Notation as It Is Actually Used.
Proceedings of the Intelligent Computer Mathematics - 12th International Conference, 2019

2018
What Does This Notation Mean Anyway?
CoRR, 2018

2017
Skalpel: A constraint-based type error slicer for Standard ML.
J. Symb. Comput., 2017

2016
Bridging Curry and Church's typing style.
J. Appl. Log., 2016

2015
Automath Type Inclusion in Barendregt's Cube.
Proceedings of the Computer Science - Theory and Applications, 2015

2014
Computerising Mathematical Text.
Proceedings of the Computational Logic, 2014

Skalpel: A Type Error Slicer for Standard ML.
Proceedings of the Ninth Workshop on Logical and Semantic Frameworks, with Applications, 2014

2012
Reducibility Proofs in the λ-Calculus.
Fundam. Informaticae, 2012

On Realisability Semantics for Intersection Types with Expansion Variables.
Fundam. Informaticae, 2012

The Algebra of Expansion.
Fundam. Informaticae, 2012

Expansion for Universal Quantifiers.
Proceedings of the Programming Languages and Systems, 2012

2010
Expressiveness of Generic Process Shape Types.
Proceedings of the Trustworthly Global Computing - 5th International Symposium, 2010

2009
Compilation of extended recursion in call-by-value functional languages.
High. Order Symb. Comput., 2009

MathLang Translation to Isabelle Syntax.
Proceedings of the Intelligent Computer Mathematics, 2009

2008
A Complete Realisability Semantics for Intersection Types and Arbitrary Expansion Variables.
Proceedings of the Theoretical Aspects of Computing, 2008

2007
Computerizing Mathematical Text with MathLang.
Proceedings of the Second Workshop on Logical and Semantic Frameworks, with Applications, 2007

Narrative Structure of Mathematical Texts.
Proceedings of the Towards Mechanized Mathematical Assistants, 14th Symposium, 2007

Restoring Natural Language as a Computerised Mathematics Input Method.
Proceedings of the Towards Mechanized Mathematical Assistants, 14th Symposium, 2007

2005
Toward an Object-Oriented Structure for Mathematical Text.
Proceedings of the Mathematical Knowledge Management, 4th International Conference, 2005

Type inference, principal typings, and let-polymorphism for first-class mixin modules.
Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, 2005

Instant Polymorphic Type Systems for Mobile Process Calculi: Just Add Reduction Rules and Close.
Proceedings of the Programming Languages and Systems, 2005

2004
Principality and type inference for intersection types using expansion variables.
Theor. Comput. Sci., 2004

Type error slicing in implicitly typed higher-order languages.
Sci. Comput. Program., 2004

Expansion: the Crucial Mechanism for Type Inference with Intersection Types: A Survey and Explanation.
Proceedings of the Third International Workshop on Intersection Types and Related Systems, 2004

Type inference with expansion variables and intersection types in system E and an exact correspondence with beta-reduction.
Proceedings of the 6th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2004

Flexible Encoding of Mathematics on the Computer.
Proceedings of the Mathematical Knowledge Management, Third International Conference, 2004

Graph-Based Proof Counting and Enumeration with Applications for Program Fragment Synthesis.
Proceedings of the Logic Based Program Synthesis and Transformation, 2004

PolyA: True Type Polymorphism for Mobile Ambients.
Proceedings of the Exploring New Frontiers of Theoretical Informatics, 2004

Call-by-Value Mixin Modules: Reduction Semantics, Side Effects, Types.
Proceedings of the Programming Languages and Systems, 2004

System E: Expansion Variables for Flexible Typing with Linear and Non-linear Types and Intersection Types.
Proceedings of the Programming Languages and Systems, 2004

2003
MathLang: Experience-driven Development of a New Mathematical Language.
Proceedings of the Mathematical Knowledge Management Symposium, 2003

Diagrams for Meaning Preservation.
Proceedings of the Rewriting Techniques and Applications, 14th International Conference, 2003

2002
A calculus with polymorphic and polyvariant flow types.
J. Funct. Program., 2002

Implementing Compositional Analysis Using Intersection Types With Expansion Variables.
Proceedings of the Intersection Types and Related Systems, 2002

The Essence of Principal Typings.
Proceedings of the Automata, Languages and Programming, 29th International Colloquium, 2002

Branching Types.
Proceedings of the Programming Languages and Systems, 2002

Fully Automatic Adaptation of Software Components Based on Semantic Specifications.
Proceedings of the Algebraic Methodology and Software Technology, 2002

2001
Cut rules and explicit substitutions.
Math. Struct. Comput. Sci., 2001

Cycle Therapy: A Prescription for Fold and Unfold on Regular Trees.
Proceedings of the 3rd international ACM SIGPLAN conference on Principles and practice of declarative programming, 2001

Functioning without Closure: Type-Safe Customized Function Representations for Standard ML.
Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming (ICFP '01), 2001

2000
Program Representation Size in an Intermediate Language with Intersection and Union Types.
Proceedings of the Types in Compilation, Third International Workshop, 2000

Introduction: Workshop on Intersection Types and Related Systems (ITRS'00).
Proceedings of the ICALP Workshops 2000, 2000

Equational Reasoning for Linking with First-Class Primitive Modules.
Proceedings of the Programming Languages and Systems, 2000

1999
Typability and Type Checking in System F are Equivalent and Undecidable.
Ann. Pure Appl. Log., 1999

Principality and Decidable Type Inference for Finite-Rank Intersection Types.
Proceedings of the POPL '99, 1999

Relating Typability and Expressiveness in Finite-Rank Intersection Type Systems (Extended Abstract).
Proceedings of the fourth ACM SIGPLAN International Conference on Functional Programming (ICFP '99), 1999

1998
Calculi of Generalized beta-Reduction and Explicit Substitutions: The Type-Free and Simply Typed Versions.
J. Funct. Log. Program., 1998

1997
A Typed Intermediate Language for Flow-Directed Compilation.
Proceedings of the TAPSOFT'97: Theory and Practice of Software Development, 1997

Strongly Typed Flow-Directed Representation Transformations.
Proceedings of the 1997 ACM SIGPLAN International Conference on Functional Programming (ICFP '97), 1997

1995
New Notions of Reduction and Non-Semantic Proofs of beta-Strong Normalization in Typed lambda-Calculi
Proceedings of the Proceedings, 1995

1994
Typability and Type-Checking in the Second-Order lambda-Calculus are Equivalent and Undecidable
Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), 1994

A Direct Algorithm for Type Inference in the Rank-2 Fragment of the Second-Order lambda-Calculus.
Proceedings of the 1994 ACM Conference on LISP and Functional Programming, 1994


  Loading...