scholarly journals Trust in the λ-calculus

1997 ◽  
Vol 7 (6) ◽  
pp. 557-591 ◽  
Author(s):  
P. ØRBÆK ◽  
J. PALSBERG

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.

1995 ◽  
Vol 2 (31) ◽  
Author(s):  
Jens Palsberg ◽  
Peter Ørbæk

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.


2015 ◽  
Vol 27 (5) ◽  
pp. 603-625 ◽  
Author(s):  
MARIO COPPO ◽  
MARIANGIOLA DEZANI-CIANCAGLINI ◽  
INES MARGARIA ◽  
MADDALENA ZACCHI

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.


1993 ◽  
Vol 19 (1-2) ◽  
pp. 87-125
Author(s):  
Paola Giannini ◽  
Furio Honsell ◽  
Simona Ronchi Della Rocca

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.


1995 ◽  
Vol 5 (1) ◽  
pp. 1-35 ◽  
Author(s):  
Mark P. Jones

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.


2013 ◽  
Vol 23 (4) ◽  
pp. 357-401 ◽  
Author(s):  
GEORGES GONTHIER ◽  
BETA ZILIANI ◽  
ALEKSANDAR NANEVSKI ◽  
DEREK DREYER

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.


2000 ◽  
Vol 11 (01) ◽  
pp. 65-87
Author(s):  
MASATOMO HASHIMOTO

This paper develops an ML-style programming language with first-class contexts i.e. expressions with holes. The crucial operation for contexts is hole-filling. Filling a hole with an expression has the effect of dynamic binding or macro expansion which provides the advanced feature of manipulating open program fragments. Such mechanisms are useful in many systems including distributed/mobile programming and program modules. If we can treat a context as a first-class citizen in a programming language, then we can manipulate open program fragments in a flexible and seamless manner. A possibility of such a programming language was shown by the theory of simply typed context calculus developed by Hashimoto and Ohori. This paper extends the simply typed system of the context calculus to an ML-style polymorphic type system, and gives an operational semantics and a sound and complete type inference algorithm.


Author(s):  
James Higginbotham

Adverbs are so named from their role in modifying verbs and other non-nominal expressions. For example, in ‘John ran slowly’, the adverb ‘slowly’ modifies ‘ran’ by characterizing the manner of John’s running. The debate on the semantic contribution of adverbs centres on two approaches. On the first approach, adverbs are understood as predicate operators: for example, in ‘John ran slowly’, ‘ran’ would be taken to be a predicate and ‘slowly’ an operator affecting its meaning. Working this out in detail requires the resources of higher-order logic. On the second approach, adverbs are understood as predicates of ‘objects’ such as events and states, reference to which is revealed in logical form. For example, ‘John ran slowly’ would be construed along the lines of ‘there was a running by John and it was slow’, in which the adverb ‘slowly’ has become a predicate ‘slow’ applied to the event that was John’s running. Since adverbs are exclusively modifiers, they are classed among the syncategorematic words of terminist logic, the investigation of which carried the subject forward from Aristotle in the thirteenth century. (The contrasting ‘categoremata’ – grammatical subjects and predicates – are those words which have meaning independently.) They are of contemporary interest for philosophical logic and semantic theory, because particular accounts of them carry implications for the nature of combinatorial semantics and language understanding, and for ontology.


2014 ◽  
Vol 25 (4) ◽  
pp. 867-891 ◽  
Author(s):  
JACQUES GARRIGUE

The type system of Objective Caml has many unique features, which make ensuring the correctness of its implementation difficult. One of these features is structurally polymorphic types, such as polymorphic object and variant types, which have the extra specificity of allowing recursion. We implemented in Coq a certified interpreter for Core ML extended with structural polymorphism and recursion. Along with type soundness of evaluation, soundness and principality of type inference, and correctness of a stack-based interpreter, are also proved.†


2014 ◽  
Vol 24 (1) ◽  
pp. 56-112 ◽  
Author(s):  
YAN CHEN ◽  
JOSHUA DUNFIELD ◽  
MATTHEW A. HAMMER ◽  
UMUT A. ACAR

AbstractComputational problems that involve dynamic data, such as physics simulations and program development environments, have been an important subject of study in programming languages. Building on this work, recent advances in self-adjusting computation have developed techniques that enable programs to respond automatically and efficiently to dynamic changes in their inputs. Self-adjusting programs have been shown to be efficient for a reasonably broad range of problems, but the approach still requires an explicit programming style, where the programmer must use specific monadic types and primitives to identify, create, and operate on data that can change over time. We describe techniques for automatically translating purely functional programs into self-adjusting programs. In this implicit approach, the programmer need only annotate the (top-level) input types of the programs to be translated. Type inference finds all other types, and a type-directed translation rewrites the source program into an explicitly self-adjusting target program. The type system is related to information-flow type systems and enjoys decidable type inference via constraint solving. We prove that the translation outputs well- typed self-adjusting programs and preserves the source program's input–output behavior, guaranteeing that translated programs respond correctly to all changes to their data. Using a cost semantics, we also prove that the translation preserves the asymptotic complexity of the source program.


Sign in / Sign up

Export Citation Format

Share Document