Fairouz Kamareddine

Jonathan P. Seldin

CoRR, 2024

Substitution in the lambda Calculus and the role of the Curry School.

[BibT_eX]

[DOI]

CoRR, 2024

2021

Generating Custom Set Theories with Non-set Structured Objects.

[BibT_eX]

[DOI]

Ciarán Dunne

Proceedings of the Intelligent Computer Mathematics - 14th International Conference, 2021

A Novel Method That Identifies The Hidden Properties Of A Person's Name In Kanji Or Hanzi.

[BibT_eX]

[DOI]

Proceedings of the MISNC 2021: The 8th Multidisciplinary International Social Networks Conference, Bergen, Norway, November 15, 2021

2020

Adding an Abstraction Barrier to ZF Set Theory.

[BibT_eX]

[DOI]

Ciarán Dunne

Proceedings of the Intelligent Computer Mathematics - 13th International Conference, 2020

2019

Intelligent Computing for Society.

[BibT_eX]

[DOI]

Imran Sarwar Bajwa

Pamini Thangarajah

J. Univers. Comput. Sci., 2019

Advance gender prediction tool of first names and its use in analysing gender disparity in Computer Science in the UK, Malaysia and China.

[BibT_eX]

[DOI]

Hua Zhao

CoRR, 2019

A Novel Phonetic Algorithm for Predicting Chinese Names using Chinese Pin Yin.

[BibT_eX]

Hua Zhao

Proceedings of the Machine Learning and Data Mining in Pattern Recognition, 2019

BNF-Style Notation as It Is Actually Used.

[BibT_eX]

[DOI]

Dee Quinlan

Joe B. Wells

Proceedings of the Intelligent Computer Mathematics - 12th International Conference, 2019

2018

What Does This Notation Mean Anyway?

[BibT_eX]

[DOI]

CoRR, 2018

2017

Skalpel: A constraint-based type error slicer for Standard ML.

[BibT_eX]

[DOI]

J. Symb. Comput., 2017

2016

Bridging Curry and Church's typing style.

[BibT_eX]

[DOI]

Jonathan P. Seldin

J. Appl. Log., 2016

2015

Explicit substitution calculi with de Bruijn indices and intersection type systems.

[BibT_eX]

[DOI]

Log. J. IGPL, 2015

Automath Type Inclusion in Barendregt's Cube.

[BibT_eX]

[DOI]

Joe B. Wells

Proceedings of the Computer Science - Theory and Applications, 2015

2014

Computerising Mathematical Text.

[BibT_eX]

[DOI]

Proceedings of the Computational Logic, 2014

Skalpel: A Type Error Slicer for Standard ML.

[BibT_eX]

[DOI]

Proceedings of the Ninth Workshop on Logical and Semantic Frameworks, with Applications, 2014

2012

A History of Types*.

[BibT_eX]

[DOI]

Proceedings of the Logic: A History of its Central Concepts, 2012

Russell's Orders in Kripke's Theory of Truth and Computational Type Theory.

[BibT_eX]

[DOI]

Robert L. Constable

Proceedings of the Sets and Extensions in the Twentieth Century, 2012

Reducibility Proofs in the λ-Calculus.

[BibT_eX]

[DOI]

Vincent Rahli

Fundam. Informaticae, 2012

On Realisability Semantics for Intersection Types with Expansion Variables.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2012

2011

Preface.

[BibT_eX]

[DOI]

Elaine Pimentel

Theor. Comput. Sci., 2011

2010

A Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi.

[BibT_eX]

[DOI]

A. V. Barbosa

Proceedings of the Fifth Logical and Semantic Frameworks, with Applications Workshop, 2010

Intersection Type Systems and Explicit Substitutions Calculi.

[BibT_eX]

[DOI]

Proceedings of the Logic, 2010

2009

Explicit substitutions calculi with one step Eta-reduction decided explicitly.

[BibT_eX]

[DOI]

Log. J. IGPL, 2009

Preface.

[BibT_eX]

[DOI]

Proceedings of the Fourth Workshop on Logical and Semantic Frameworks, with Applications, 2009

Principal Typings in a Restricted Intersection Type System for Beta Normal Forms with De Bruijn Indices

[BibT_eX]

[DOI]

Proceedings of the Proceedings Ninth International Workshop on Reduction Strategies in Rewriting and Programming, 2009

MathLang Translation to Isabelle Syntax.

[BibT_eX]

[DOI]

Robert Lamar

Proceedings of the Intelligent Computer Mathematics, 2009

2008

Higher-Order Unification: A structural relation between Huet's method and the one based on explicit substitutions.

[BibT_eX]

[DOI]

J. Appl. Log., 2008

Simplified Reducibility Proofs of Church-Rosser for beta- and betaeta-reduction.

[BibT_eX]

[DOI]

Vincent Rahli

Proceedings of the Third Workshop on Logical and Semantic Frameworks with Applications, 2008

A Complete Realisability Semantics for Intersection Types and Arbitrary Expansion Variables.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computing, 2008

Principal Typings for Explicit Substitutions Calculi.

[BibT_eX]

[DOI]

Proceedings of the Logic and Theory of Algorithms, 2008

2007

The Weak Normalization of the Simply Typed lambda-se-calculus.

[BibT_eX]

[DOI]

Ariel Arbiser

Log. J. IGPL, 2007

Computerizing Mathematical Text with MathLang.

[BibT_eX]

[DOI]

Proceedings of the Second Workshop on Logical and Semantic Frameworks, with Applications, 2007

Capsule reviews.

[BibT_eX]

[DOI]

Comput. J., 2007

A completeness result for a realisability semantics for an intersection type system.

[BibT_eX]

[DOI]

Karim Nour

Ann. Pure Appl. Log., 2007

The Gradual Computerisation of Mathematics in MathLang.

[BibT_eX]

[DOI]

Proceedings of the Ninth International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2007

Narrative Structure of Mathematical Texts.

[BibT_eX]

[DOI]

Proceedings of the Towards Mechanized Mathematical Assistants, 14th Symposium, 2007

Restoring Natural Language as a Computerised Mathematics Input Method.

[BibT_eX]

[DOI]

Proceedings of the Towards Mechanized Mathematical Assistants, 14th Symposium, 2007

2006

SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi.

[BibT_eX]

[DOI]

J. Appl. Non Class. Logics, 2006

2005

De Bruijn's syntax and reductional behaviour of lambda-terms: the typed case.

[BibT_eX]

[DOI]

J. Log. Algebraic Methods Program., 2005

De Bruijn's syntax and reductional behaviour of lambda-terms: the untyped case.

[BibT_eX]

[DOI]

J. Log. Algebraic Methods Program., 2005

Typed lambda-calculi with one binder.

[BibT_eX]

[DOI]

J. Funct. Program., 2005

Comparing and implementing calculi of explicit substitutions with eta-reduction.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2005

Toward an Object-Oriented Structure for Mathematical Text.

[BibT_eX]

[DOI]

Manuel Maarek

Proceedings of the Mathematical Knowledge Management, 4th International Conference, 2005

2004

A Refinement of de Bruijn's Formal Language of Mathematics.

[BibT_eX]

[DOI]

J. Log. Lang. Inf., 2004

Editorial.

[BibT_eX]

[DOI]

J. Appl. Log., 2004

Flexible Encoding of Mathematics on the Computer.

[BibT_eX]

[DOI]

Manuel Maarek

Proceedings of the Mathematical Knowledge Management, Third International Conference, 2004

Second-Order Matching via Explicit Substitutions.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2004

2003

On Automating the Extraction of Programs from Termination Proofs.

[BibT_eX]

[DOI]

Rev. Colomb. de Computación, 2003

Revisiting the notion of function.

[BibT_eX]

[DOI]

J. Log. Algebraic Methods Program., 2003

Formalizing Strong Normalization Proofs of Explicit Substitution Calculi in ALF.

[BibT_eX]

[DOI]

Qiao Haiyan

J. Autom. Reason., 2003

Explicit substitutions à la de Bruijn: the local and global way.

[BibT_eX]

[DOI]

Proceedings of the Mathematics, 2003

MathLang: Experience-driven Development of a New Mathematical Language.

[BibT_eX]

[DOI]

Manuel Maarek

Proceedings of the Mathematical Knowledge Management Symposium, 2003

Automath and Pure Type Systems.

[BibT_eX]

[DOI]

Proceedings of the Mathematics, 2003

Mathematical Knowledge Management Symposium 2003.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Knowledge Management Symposium, 2003

Preface.

[BibT_eX]

[DOI]

Herman Geuvers

Proceedings of the Mathematics, 2003

Diagrams for Meaning Preservation.

[BibT_eX]

[DOI]

Detlef Plump

Proceedings of the Rewriting Techniques and Applications, 14th International Conference, 2003

2002

Special Issue Mechanizing and Automating Mathematics: In honour of N.G. de Bruijn - Preface.

[BibT_eX]

[DOI]

J. Autom. Reason., 2002

An Extension of an Automated Termination Method of Recursive Functions.

[BibT_eX]

[DOI]

Int. J. Found. Comput. Sci., 2002

Formalizing Belief Revision in Type Theory.

[BibT_eX]

[DOI]

Tijn Borghuis

Log. J. IGPL, 2002

On automating the extraction of programs from proofs using product types.

[BibT_eX]

[DOI]

Proceedings of the 9th Workhop on Logic, Language, Information and Computation, 2002

Comparing Calculi of Explicit Substitutions with Eta-reduction.

[BibT_eX]

[DOI]

Proceedings of the 9th Workhop on Logic, Language, Information and Computation, 2002

Pure Type Systems with de Bruijn Indices.

[BibT_eX]

[DOI]

Comput. J., 2002

Types in logic and mathematics before 1940.

[BibT_eX]

[DOI]

Bull. Symb. Log., 2002

On Functions and Types: A Tutorial.

[BibT_eX]

[DOI]

Proceedings of the SOFSEM 2002: Theory and Practice of Informatics, 2002

Parameters in Pure Type Systems.

[BibT_eX]

[DOI]

Proceedings of the LATIN 2002: Theoretical Informatics, 2002

2001

Reviewing the Classical and the de Bruijn Notation for [lambda]-calculus and Pure Type Systems.

[BibT_eX]

[DOI]

J. Log. Comput., 2001

A Correspondence between Martin-Löf Type Theory, the Ramified Theory of Types and Pure Type Systems.

[BibT_eX]

[DOI]

J. Log. Lang. Inf., 2001

Unification via the lambda se-Style of Explicit Substitutions.

[BibT_eX]

[DOI]

Log. J. IGPL, 2001

De Bruijn's Syntax and Reductional Equivalence of Lambda-Terms.

[BibT_eX]

[DOI]

Proceedings of the 3rd international ACM SIGPLAN conference on Principles and practice of declarative programming, 2001

Refining the Barendregt Cube Using Parameters.

[BibT_eX]

[DOI]

Proceedings of the Functional and Logic Programming, 5th International Symposium, 2001

2000

Relating the λσ- and λs-styles of explicit substitutions.

[BibT_eX]

[DOI]

J. Log. Comput., 2000

Editorial.

[BibT_eX]

[DOI]

Jan Willem Klop

J. Log. Comput., 2000

Postponement, conservation and preservation of strong normalization for generalized reduction.

[BibT_eX]

[DOI]

J. Log. Comput., 2000

Unification via se-style of explicit substitution.

[BibT_eX]

[DOI]

Proceedings of the 2nd international ACM SIGPLAN conference on on Principles and practice of declarative programming, 2000

1999

On Pi-Conversion in the lambda-Cube and the Combination with Abbreviations.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 1999

On Formalised Proofs of Termination of Recursive Functions.

[BibT_eX]

[DOI]

Proceedings of the Principles and Practice of Declarative Programming, International Conference PPDP'99, Paris, France, September 29, 1999

On Automating Inductive and Non-inductive Termination Methods.

[BibT_eX]

[DOI]

Proceedings of the Advances in Computing Science, 1999

1998

Calculi of Generalized beta-Reduction and Explicit Substitutions: The Type-Free and Simply Typed Versions.

[BibT_eX]

[DOI]

J. Funct. Log. Program., 1998

The Soundness of Explicit Substitution with Nameless Variables.

[BibT_eX]

[DOI]

Int. J. Found. Comput. Sci., 1998

Bridging de Bruijn Indices and Variable Names in Explicit Substitutions Calculi.

[BibT_eX]

[DOI]

Log. J. IGPL, 1998

1997

Extending a lambda-Calculus with Explicit Substitution which Preserves Strong Normalisation Into a Confluent Calculus on Open Terms.

[BibT_eX]

[DOI]

J. Funct. Program., 1997

Explicit Substitutions for the Lambda-Calculus.

[BibT_eX]

[DOI]

Gilles Barthe

Proceedings of the Algebraic and Logic Programming, 6th International Joint Conference, 1997

1996

A Useful lambda-Notation.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1996

Canonical Typing and Pi-Conversion in the Barendregt Cube.

[BibT_eX]

[DOI]

J. Funct. Program., 1996

A Reflection on Russell's Ramified Types and Kripke's Hierarchy of Truths.

[BibT_eX]

[DOI]

Log. J. IGPL, 1996

The Barendregt Cube with Definitions and Generalised Reduction.

[BibT_eX]

[DOI]

Inf. Comput., 1996

Generalized beta-Reduction and Explicit Substitution.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages: Implementations, 1996

1995

A Type Free Theory and Collective/Distributive Predication.

[BibT_eX]

[DOI]

J. Log. Lang. Inf., 1995

Refining Reduction in the Lambda Calculus.

[BibT_eX]

[DOI]

J. Funct. Program., 1995

Important Issues in Foundational Formalisms.

[BibT_eX]

[DOI]

Log. J. IGPL, 1995

A Lambda-Calculus à la de Bruijn with Explicit Substitutions

[BibT_eX]

[DOI]

Proceedings of the Programming Languages: Implementations, 1995

1994

A Unified Approach to Type Theory Through a Refined lambda-Calculus.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1994

1993

Polymorphism, Type containment and Nominalization.

[BibT_eX]

[DOI]

Ewan Klein

J. Log. Lang. Inf., 1993

On Stepwise Explicit Substitution.

[BibT_eX]

[DOI]

Int. J. Found. Comput. Sci., 1993

1992

A System at the Cross-Roads of Functional and Logic Programming.

[BibT_eX]

[DOI]

Sci. Comput. Program., 1992

Set Theory and Nominalization, Part II.

[BibT_eX]

[DOI]

J. Log. Comput., 1992

Set Theory and Nominalization, Part I.

[BibT_eX]

[DOI]

J. Log. Comput., 1992

λ-Terms, Logic, Determiners and Quantifiers.

[BibT_eX]

[DOI]