scholarly journals Trust in the lambda-calculus

1995 ◽  
Vol 2 (31) ◽  
Author(s):  
Jens Palsberg ◽  
Peter Ørbæk
Keyword(s):  
Type System ◽  
Lambda Calculus ◽  
Higher Order ◽  
Type Inference ◽  
Function Type ◽  
Reduction Property ◽  
Type Constructor ◽  
The Subject ◽  
Run Time ◽  
Trust Information

This paper introduces trust analysis for higher-order languages. Trust<br />analysis encourages the programmer to make explicit the trustworthiness of<br />data, and in return it can guarantee that no mistakes with respect to trust will<br />be made at run-time. We present a confluent lambda-calculus with explicit trust<br />operations, and we equip it with a trust-type system which has the subject<br />reduction property. Trust information in presented as two annotations of each<br />function type constructor, and type inference is computable in O(n^3) time.

scholarly journals Trust in the λ-calculus

1997 ◽  
Vol 7 (6) ◽  
pp. 557-591 ◽  
Author(s):  
P. ØRBÆK ◽  
J. PALSBERG
Keyword(s):  
Type System ◽  
Higher Order ◽  
Type Inference ◽  
Reduction Property ◽  
The Subject ◽  
Run Time ◽  
Trust Information

This paper introduces trust analysis for higher-order languages. Trust analysis encourages the programmer to make explicit the trustworthiness of data, and in return it can guarantee that no mistakes with respect to trust will be made at run-time. We present a confluent λ-calculus with explicit trust operations, and we equip it with a trust-type system which has the subject reduction property. Trust information is presented as annotations of the underlying Curry types, and type inference is computable in O(n3) time.

scholarly journals A Complete Calculus of Monotone and Antitone Higher-Order Functions

10.29007/3n54 ◽  
2018 ◽  
Author(s):  
Thomas Icard ◽  
Lawrence Moss
Keyword(s):  
Type System ◽  
Lambda Calculus ◽  
Higher Order ◽  
Typed Lambda Calculus ◽  
Higher Order Functions

This paper adds monotonicity and antitonicity information to the typed lambda calculus, thereby providing a foundation for the Monotonicity Calculus first developed by van Benthem and others. We establish properties of the type system, propose a syntax, semantics, and proof calculus, and prove completeness for the calculus with respect to hierarchies of monotone and antitone functions over base preorders.

scholarly journals Isomorphism of intersection and union types

2015 ◽  
Vol 27 (5) ◽  
pp. 603-625 ◽  
Author(s):  
MARIO COPPO ◽  
MARIANGIOLA DEZANI-CIANCAGLINI ◽  
INES MARGARIA ◽  
MADDALENA ZACCHI
Keyword(s):  
Normal Form ◽  
Normal Forms ◽  
Type System ◽  
Type Reduction ◽  
Reduction Property ◽  
The Subject ◽  
Complete Characterisation

This paper gives a complete characterisation of type isomorphism definable by terms of a λ-calculus with intersection and union types. Unfortunately, when union is considered the Subject Reduction property does not hold in general. However, it is well known that in the λ-calculus, independently of the considered type system, the isomorphism between two types can be realised only by invertible terms. Notably, all invertible terms are linear terms. In this paper, the isomorphism of intersection and union types is investigated using a relevant type system for linear terms enjoying the Subject Reduction property. To characterise type isomorphism, a similarity between types and a type reduction are introduced. Types have a unique normal form with respect to the reduction rules and two types are isomorphic if and only if their normal forms are similar.

scholarly journals Preface

1999 ◽  
Vol 9 (4) ◽  
pp. 321-321
Author(s):  
MARIANGIOLA DEZANI-CIANCAGLINI ◽  
GIUSEPPE LONGO ◽  
JONATHAN P. SELDIN
Keyword(s):  
Computer Science ◽  
Type System ◽  
Lambda Calculus ◽  
Combinatory Logic ◽  
Subsequent Work ◽  
Mathematical Structures ◽  
Type Assignment ◽  
The Face ◽  
The Subject ◽  
The University

This special double issue of Mathematical Structures in Computer Science is in honour of Roger Hindley and is devoted to the topic of lambda-calculus and logic.It is a great pleasure for us to greet Roger Hindley on the occasion of his retirement from the University of Wales, Swansea, and his 60th birthday. We have known Roger for many years and we have had the chance to collaborate with him and appreciate his intellectual standard, his remarkable mathematical rigor, and his inexhaustible sense of humour. This has enabled Roger to step back critically even in the face of a difficult mathematical task and help to solve it by a new way of looking at it.Roger Hindley's dissertation concerned the Church–Rosser Theorem and was a significant contribution to the topic. His subsequent work spanned many aspects of lambda-calculus, covering both its models and applications. To mention just a few, he produced work on axioms for Curry's strong (eta) reduction, comparing lambda and combinatory reductions (and models), models for type assignment, and formulas as types for some nonstandard systems (intersection types, BCK systems, etc.).Roger Hindley collaborated with Jonathan Seldin on two well-known introductory books on the subject (Bruce Lercher also collaborated as an author on the first of these). More recently, he has published an introduction to type assignment. He was also co-author with H. B. Curry and J. Seldin on Combinatory Logic, vol. II, which is an important research publication on the subject.Roger has played an important role in the lambda-calculus community over the years as that community has grown; in particular, he has been an active organiser of many conferences on the topic. In fact, his success in disseminating knowledge about the lambda calculus, particularly in the United Kingdom, means that Roger may be considered a ‘Godfather’ of ML and its type system.(In preparing this special issue of Mathematical Structures in Computer Science, we have been fortunate enough to receive too many excellent papers for one double issue. As a result, additional papers by colleagues who wish to honour Roger will appear in future issues of this journal.)

Monadic encapsulation of effects: a revised approach (extended version)

2001 ◽  
Vol 11 (6) ◽  
pp. 591-627 ◽  
Author(s):  
E. MOGGI ◽  
AMR SABRY
Keyword(s):  
Ad Hoc ◽  
Operational Semantics ◽  
Type System ◽  
Lambda Calculus ◽  
Higher Order ◽  
Functional Language ◽  
Simple Modification ◽  
Type Safety ◽  
Original Proposal ◽  
Type Parameter

Launchbury and Peyton Jones came up with an ingenious idea for embedding regions of imperative programming in a pure functional language like Haskell. The key idea was based on a simple modification of Hindley-Milner's type system. Our first contribution is to propose a more natural encapsulation construct exploiting higher-order kinds, which achieves the same encapsulation effect, but avoids the ad hoc type parameter of the original proposal. The second contribution is a type safety result for encapsulation of strict state using both the original encapsulation construct and the newly introduced one. We establish this result in a more expressive context than the original proposal, namely in the context of the higher-order lambda-calculus. The third contribution is a type safety result for encapsulation of lazy state in the higher-order lambda-calculus. This result resolves an outstanding open problem on which previous proof attempts failed. In all cases, we formalize the intended implementations as simple big-step operational semantics on untyped terms, which capture interesting implementation details not captured by the reduction semantics proposed previously.

Type Inference: Some Results, Some Problems1

1993 ◽  
Vol 19 (1-2) ◽  
pp. 87-125
Author(s):  
Paola Giannini ◽  
Furio Honsell ◽  
Simona Ronchi Della Rocca
Keyword(s):  
Large Class ◽  
Higher Order ◽  
Type Inference ◽  
Principal Type ◽  
Open Problems ◽  
Inference Problem ◽  
Type Assignment ◽  
Unification Problem

In this paper we investigate the type inference problem for a large class of type assignment systems for the λ-calculus. This is the problem of determining if a term has a type in a given system. We discuss, in particular, a collection of type assignment systems which correspond to the typed systems of Barendregt’s “cube”. Type dependencies being shown redundant, we focus on the strongest of all, Fω, the type assignment version of the system Fω of Girard. In order to manipulate uniformly type inferences we give a syntax directed presentation of Fω and introduce the notions of scheme and of principal type scheme. Making essential use of them, we succeed in reducing the type inference problem for Fω to a restriction of the higher order semi-unification problem and in showing that the conditional type inference problem for Fω is undecidable. Throughout the paper we call attention to open problems and formulate some conjectures.

A system of constructor classes: overloading and implicit higher-order polymorphism

1995 ◽  
Vol 5 (1) ◽  
pp. 1-35 ◽  
Author(s):  
Mark P. Jones
Keyword(s):  
Type System ◽  
Type Systems ◽  
Natural Generalization ◽  
Higher Order ◽  
Functional Language ◽  
Effective Algorithm ◽  
Prototype Implementation ◽  
Type Classes

AbstractThis paper describes a flexible type system that combines overloading and higher-order polymorphism in an implicitly typed language using a system of constructor classes—a natural generalization of type classes in Haskell. We present a range of examples to demonstrate the usefulness of such a system. In particular, we show how constructor classes can be used to support the use of monads in a functional language. The underlying type system permits higher-order polymorphism but retains many of the attractive features that have made Hindley/Milner type systems so popular. In particular, there is an effective algorithm that can be used to calculate principal types without the need for explicit type or kind annotations. A prototype implementation has been developed providing, amongst other things, the first concrete implementation of monad comprehensions known to us at the time of writing.

scholarly journals Binding Time Analysis: Abstract Interpretation vs. Type Inference

1992 ◽  
Vol 21 (393) ◽  
Author(s):  
Jens Palsberg ◽  
Michael I. Schwartzbach
Keyword(s):  
Abstract Interpretation ◽  
Lambda Calculus ◽  
Type Inference ◽  
Time Analysis ◽  
Binding Time ◽  
Better Than ◽  
Binding Time Analysis

Binding time analysis is important in partial evaluators. Its task is to determine which parts of a program can be specialized if some of the expected input is known. Two approaches to do this are abstract interpretation and type inference. We compare two specific such analyses to see which one determines most program parts to be eliminable. The first is the abstract interpretation approach of Bondorf, and the second is the type inference approach o£ Gomard. Both apply to the untyped lambda calculus. We prove that Bondorf's analysis is better than Gomard's.

scholarly journals How to make ad hoc proof automation less ad hoc

2013 ◽  
Vol 23 (4) ◽  
pp. 357-401 ◽  
Author(s):  
GEORGES GONTHIER ◽  
BETA ZILIANI ◽  
ALEKSANDAR NANEVSKI ◽  
DEREK DREYER
Keyword(s):  
Design Patterns ◽  
Ad Hoc ◽  
Type System ◽  
Type Inference ◽  
Interactive Theorem Provers ◽  
Proof Automation ◽  
Novel Approach ◽  
Type Classes ◽  
Structure Programming ◽  
Base Logic

AbstractMost interactive theorem provers provide support for some form of user-customizable proof automation. In a number of popular systems, such as Coq and Isabelle, this automation is achieved primarily through tactics, which are programmed in a separate language from that of the prover's base logic. While tactics are clearly useful in practice, they can be difficult to maintain and compose because, unlike lemmas, their behavior cannot be specified within the expressive type system of the prover itself.We propose a novel approach to proof automation in Coq that allows the user to specify the behavior of custom automated routines in terms of Coq's own type system. Our approach involves a sophisticated application of Coq's canonical structures, which generalize Haskell type classes and facilitate a flexible style of dependently-typed logic programming. Specifically, just as Haskell type classes are used to infer the canonical implementation of an overloaded term at a given type, canonical structures can be used to infer the canonical proof of an overloaded lemma for a given instantiation of its parameters. We present a series of design patterns for canonical structure programming that enable one to carefully and predictably coax Coq's type inference engine into triggering the execution of user-supplied algorithms during unification, and we illustrate these patterns through several realistic examples drawn from Hoare Type Theory. We assume no prior knowledge of Coq and describe the relevant aspects of Coq type inference from first principles.

Sign in / Sign up

Export Citation Format

Share Document