scholarly journals Type Checking Semantic Functions in ASDF

2004 ◽  
Vol 11 (35) ◽  
Author(s):  
Jørgen Iversen
Keyword(s):  
Side Effects ◽  
Programming Languages ◽  
Type System ◽  
Type Checking ◽  
Semantic Function ◽  
Semantic Framework ◽  
Language Constructs ◽  
Type Check

When writing semantic descriptions of programming languages, it is convenient to have tools for checking the descriptions. With frameworks that use inductively defined semantic functions to map programs to their denotations, we would like to check that the semantic functions result in denotations with certain properties. In this paper we present a type system for a modular style of the action semantic framework that, given signatures of all the semantic functions used in a semantic equation defining a semantic function, performs a soft type check on the action in the semantic equation.<br /> <br />We introduce types for actions that describe different properties of the actions, like the type of data they expect and produce, whether they can fail or have side effects, etc. A type system for actions which uses these new action types is presented. Using the new action types in the signatures of semantic functions, the language describer can assert properties of semantic functions and have the assertions checked by an implementation of the type system.<br /> <br />The type system has been implemented for use in connection with the recently developed formalism ASDF. The formalism supports writing language definitions by combining modules that describe single language constructs. This is possible due to the inherent modularity in ASDF. We show how we manage to preserve the modularity and still perform specialised type checks for each module.

scholarly journals A framework for improving error messages in dependently-typed languages

2019 ◽  
Vol 9 (1) ◽  
pp. 1-32 ◽  
Author(s):  
Joseph Eremondi ◽  
Wouter Swierstra ◽  
Jurriaan Hage
Keyword(s):  
Programming Languages ◽  
Type System ◽  
Higher Order ◽  
Type Checking ◽  
Unification Algorithm ◽  
Implicit Arguments ◽  
Unification Problem ◽  
Heuristic Analysis ◽  
Type Check ◽  
Typed Languages

AbstractDependently-typed programming languages provide a powerful tool for establishing code correctness. However, it can be hard for newcomers to learn how to employ the advanced type system of such languages effectively. For simply-typed languages, several techniques have been devised to generate helpful error messages and suggestions for the programmer. We adapt these techniques to dependently-typed languages, to facilitate their more widespread adoption. In particular, we modify a higher-order unification algorithm that is used to resolve and type-check implicit arguments. We augment this algorithm with replay graphs, allowing for a global heuristic analysis of a unification problem-set, error-tolerant typing, which allows type-checking to continue after errors are found, and counter-factual unification, which makes error messages less affected by the order in which types are checked. A formalization of our algorithm is presented with an outline of its correctness. We implement replay graphs, and compare the generated error messages to those from existing languages, highlighting the improvements we achieved.

scholarly journals Implementing type theory in higher order constraint logic programming

2019 ◽  
Vol 29 (8) ◽  
pp. 1125-1150
Author(s):  
FERRUCCIO GUIDI ◽  
CLAUDIO SACERDOTI COEN ◽  
ENRICO TASSI
Keyword(s):  
Programming Languages ◽  
Programming Language ◽  
Type System ◽  
Theorem Prover ◽  
Type Checking ◽  
Language Extension ◽  
Order Constraint ◽  
Simple Implementation ◽  
Calculus Of Inductive Constructions ◽  
High Level

In this paper, we are interested in high-level programming languages to implement the core components of an interactive theorem prover for a dependently typed language: the kernel – responsible for type-checking closed terms – and the elaborator – that manipulates open terms, that is terms containing unresolved unification variables.In this paper, we confirm that λProlog, the language developed by Miller and Nadathur since the 80s, is extremely suitable for implementing the kernel. Indeed, we easily obtain a type checker for the Calculus of Inductive Constructions (CIC). Even more, we do so in an incremental way by escalating a checker for a pure type system to the full CIC.We then turn our attention to the elaborator with the objective to obtain a simple implementation thanks to the features of the programming language. In particular, we want to use λProlog’s unification variables to model the object language ones. In this way, scope checking, carrying of assignments and occur checking are handled by the programming language.We observe that the eager generative semantics inherited from Prolog clashes with this plan. We propose an extension to λProlog that allows to control the generative semantics, suspend goals over flexible terms turning them into constraints, and finally manipulate these constraints at the meta-meta level via constraint handling rules.We implement the proposed language extension in the Embedded Lambda Prolog Interpreter system and we discuss how it can be used to extend the kernel into an elaborator for CIC.

A paradigmatic object-oriented programming language: Design, static typing and semantics

1994 ◽  
Vol 4 (2) ◽  
pp. 127-206 ◽  
Author(s):  
Kim B. Bruce
Keyword(s):  
Fixed Points ◽  
Programming Languages ◽  
Programming Language ◽  
Type System ◽  
Object Oriented ◽  
Object Oriented Programming ◽  
Language Design ◽  
Type Checking ◽  
Basic Features ◽  
Oriented Programming Language

AbstractTo illuminate the fundamental concepts involved in object-oriented programming languages, we describe the design of TOOPL, a paradigmatic, statically-typed, functional, object-oriented programming language which supports classes, objects, methods, hidden instance variables, subtypes and inheritance.It has proven to be quite difficult to design such a language which has a secure type system. A particular problem with statically type checking object-oriented languages is designing typechecking rules which ensure that methods provided in a superclass will continue to be type correct when inherited in a subclass. The type-checking rules for TOOPL have this feature, enabling library suppliers to provide only the interfaces of classes with actual executable code, while still allowing users to safely create subclasses. To achieve greater expressibility while retaining type-safety, we choose to separate the inheritance and subtyping hierarchy in the language.The design of TOOPL has been guided by an analysis of the semantics of the language, which is given in terms of a model of the F-bounded second-order lambda calculus with fixed points at both the element and type level. This semantics supports the language design by providing a means to prove that the type-checking rules are sound, thus guaranteeing that the language is type-safe.While the semantics of our language is rather complex, involving fixed points at both the element and type level, we believe that this reflects the inherent complexity of the basic features of object-oriented programming languages. Particularly complex features include the implicit recursion inherent in the use of the keyword, self, to refer to the current object, and its corresponding type, MyType. The notions of subclass and inheritance introduce the greatest semantic complexities, whereas the notion of subtype is more straightforward to deal with. Our semantic investigations lead us to recommend caution in the use of inheritance, since small changes to method definitions in subclasses can result in major changes to the meanings of the other methods of the class.

scholarly journals iRho: an imperative rewriting calculus

2008 ◽  
Vol 18 (3) ◽  
pp. 467-500
Author(s):  
LUIGI LIQUORI ◽  
BERNARD PAUL SERPETTE
Keyword(s):  
Side Effects ◽  
Pattern Matching ◽  
Operational Semantics ◽  
Type System ◽  
Order Type ◽  
Proof Assistant ◽  
Type Checking ◽  
First Order ◽  
Static Semantics ◽  
The Core

We propose an imperative version of the Rewriting Calculus, a calculus based on pattern matching, pattern abstraction and side effects, which we call iRho.We formulate both a static and big-stepcall-by-valueoperational semantics of iRho. The operational semantics is deterministic, and immediately suggests how an interpreter for the calculus may be built. The static semantics is given using a first-order type system based on a form of product types, which can be assigned to term-like structures (that is, records).The calculus isà laChurch, that is, pattern abstractions are decorated with the types of the free variables of the pattern.iRho is a good candidate for the core of a pattern-matching imperative language, where a (monomorphic) typed store can be safely manipulated and where fixed points are built into the language itself.Properties such as determinism of the interpreter and subject-reduction have been completely checked using a machine-assisted approach with theCoqproof assistant. Progress and decidability of type checking are proved using pen and paper.

scholarly journals Description of the Imperative Programming Language in Haskell

2021 ◽  
Vol 4 ◽  
pp. 72-77
Author(s):  
Volodymyr Protsenko
Keyword(s):  
Programming Languages ◽  
Programming Language ◽  
Formal Specification ◽  
Type System ◽  
Main Task ◽  
Abstract Syntax ◽  
Data Types ◽  
Good Tool ◽  
Semantic Function ◽  
Finite Set

When creating a programming language, it is necessary to determine its syntax and semantics. The main task of syntax is to describe all constructions that are elements of the language. For this purpose, a specific syntax highlights syntactically correct sequences of characters of the language alphabet. Most often it is a finite set of rules that generate an infinite set of all construction languages, such as the extended Backus-Naur (BNF) form.To describe the semantics of the language, the preference is given to the abstract syntax, which in real programming languages is shorter and more obvious than specific. The relationship between abstract syntax objects and the syntax of the program in compilers solves the parsing phase.Denotational semantics is used to describe semantics. Initially, it records the denotations of the simplest syntactic objects. Then, with each compound syntactic construction, a semantic function is associated, which by denotations of components of a design calculates its value – denotation. Since the program is a specific syntactic construction, its denotation is possible to determine using the appropriate semantic function. Note that the program itself is not executed when calculating its denotation.The denotative description of a programming language includes the abstract syntax of its constructions, denotations – the meanings of constructions and semantic functions that reflect elements of abstract syntax (language constructions) in their denotations (meanings).The use of the functional programming language Haskell as a metalanguage is considered. The Haskell type system is a good tool for constructing abstract syntax. The various possibilities for describing pure functions, which are often the denotations of programming language constructs, are the basis for the effective use of Haskell to describe denotational semantics.The paper provides a formal specification of a simple imperative programming language with integer data, block structure, and the traditional set of operators: assignment, input, output, loop and conditional. The ability of Haskell to effectively implement parsing, which solves the problem of linking a particular syntax with the abstract, allows to expand the formal specification of the language to its implementation: a pure function — the interpreter.The work contains all the functions and data types that make up the interpreter of a simple imperative programming language.

A Lightweight Formalism for Reference Lifetimes and Borrowing in Rust

2021 ◽  
Vol 43 (1) ◽  
pp. 1-73
Author(s):  
David J. Pearce
Keyword(s):  
Memory Management ◽  
Programming Model ◽  
Type System ◽  
Control Flow ◽  
Two Phase ◽  
Type Checking ◽  
Strong Focus ◽  
Reference Implementation ◽  
Two Phases ◽  
Complex Features

Rust is a relatively new programming language that has gained significant traction since its v1.0 release in 2015. Rust aims to be a systems language that competes with C/C++. A claimed advantage of Rust is a strong focus on memory safety without garbage collection. This is primarily achieved through two concepts, namely, reference lifetimes and borrowing . Both of these are well-known ideas stemming from the literature on region-based memory management and linearity / uniqueness . Rust brings both of these ideas together to form a coherent programming model. Furthermore, Rust has a strong focus on stack-allocated data and, like C/C++ but unlike Java, permits references to local variables. Type checking in Rust can be viewed as a two-phase process: First, a traditional type checker operates in a flow-insensitive fashion; second, a borrow checker enforces an ownership invariant using a flow-sensitive analysis. In this article, we present a lightweight formalism that captures these two phases using a flow-sensitive type system that enforces “ type and borrow safety .” In particular, programs that are type and borrow safe will not attempt to dereference dangling pointers. Our calculus core captures many aspects of Rust, including copy- and move-semantics, mutable borrowing, reborrowing, partial moves, and lifetimes. In particular, it remains sufficiently lightweight to be easily digested and understood and, we argue, still captures the salient aspects of reference lifetimes and borrowing. Furthermore, extensions to the core can easily add more complex features (e.g., control-flow, tuples, method invocation). We provide a soundness proof to verify our key claims of the calculus. We also provide a reference implementation in Java with which we have model checked our calculus using over 500B input programs. We have also fuzz tested the Rust compiler using our calculus against 2B programs and, to date, found one confirmed compiler bug and several other possible issues.

scholarly journals Constructive Action Semantics for Core ML

2004 ◽  
Vol 11 (37) ◽  
Author(s):  
Jørgen Iversen ◽  
Peter D. Mosses
Keyword(s):  
Programming Languages ◽  
Tool Support ◽  
Semantic Description ◽  
Action Semantics ◽  
Language Constructs ◽  
Description Framework ◽  
The Individual ◽  
Language Construct ◽  
Language Description

Usually, the majority of language constructs found in a programming language can also be found in many other languages, because language design is based on reuse. This should be reflected in the way we give semantics to programming languages. It can be achieved by making a language description consist of a collection of modules, each defining a single language construct. The description of a single language construct should be language independent, so that it can be reused in other descriptions without any changes. We call a language description framework ``constructive'' when it supports independent description of individual constructs.<br /> <br />We present a case study in constructive semantic description. The case study is a description of Core ML, consisting of a mapping from it to BAS (Basic Abstract Syntax) and action semantic descriptions of the individual BAS constructs. The latter are written in ASDF (Action Semantics Definition Formalism), a formalism specially designed for writing action semantic descriptions of single language constructs. Tool support is provided by the ASF+SDF Meta-Environment and by the Action Environment, which is a new extension of the ASF+SDF Meta-Environment.

Coherence of subsumption, minimum typing and type-checking in F ≤

1992 ◽  
Vol 2 (1) ◽  
pp. 55-91 ◽  
Author(s):  
Pierre-Louis Curien ◽  
Giorgio Ghelli
Keyword(s):  
Normal Form ◽  
Type System ◽  
Lambda Calculus ◽  
Complete Information ◽  
Second Order ◽  
Semantic Interpretation ◽  
Type Checking ◽  
Rewriting System ◽  
Different Types ◽  
Rewriting Rules

A subtyping relation ≤ between types is often accompanied by a typing rule, called subsumption: if a term a has type T and T≤U, then a has type U. In presence of subsumption, a well-typed term does not codify its proof of well typing. Since a semantic interpretation is most naturally defined by induction on the structure of typing proofs, a problem of coherence arises: different typing proofs of the same term must have related meanings. We propose a proof-theoretical, rewriting approach to this problem. We focus on F≤, a second-order lambda calculus with bounded quantification, which is rich enough to make the problem interesting. We define a normalizing rewriting system on proofs, which transforms different proofs of the same typing judgement into a unique normal proof, with the further property that all the normal proofs assigning different types to a given term in a given environment differ only by a final application of the subsumption rule. This rewriting system is not defined on the proofs themselves but on the terms of an auxiliary type system, in which the terms carry complete information about their typing proof. This technique gives us three different results:— Any semantic interpretation is coherent if and only if our rewriting rules are satisfied as equations.— We obtain a proof of the existence of a minimum type for each term in a given environment.— From an analysis of the shape of normal form proofs, we obtain a deterministic typechecking algorithm, which is sound and complete by construction.

Introduction to the Special Issue on Dependent Type Theory Meets Practical Programming

2004 ◽  
Vol 14 (1) ◽  
pp. 1-2
Author(s):  
GILLES BARTHE ◽  
PETER DYBJEN ◽  
PETER THIEMANN
Keyword(s):  
Programming Languages ◽  
Type Theory ◽  
Type System ◽  
Type Systems ◽  
Special Issue ◽  
Dependent Type Theory ◽  
Dependent Type

Modern programming languages rely on advanced type systems that detect errors at compile-time. While the benefits of type systems have long been recognized, there are some areas where the standard systems in programming languages are not expressive enough. Language designers usually trade expressiveness for decidability of the type system. Some interesting programs will always be rejected (despite their semantical soundness) or be assigned uninformative types.

JOIN POINT DESIGNATION DIAGRAMS: A GRAPHICAL REPRESENTATION OF JOIN POINT SELECTIONS

2006 ◽  
Vol 16 (03) ◽  
pp. 317-346 ◽  
Author(s):  
DOMINIK STEIN ◽  
STEFAN HANENBERG ◽  
RAINER UNLAND
Keyword(s):  
Software Development ◽  
Programming Languages ◽  
Graphical Representation ◽  
Point Selection ◽  
Aspect Oriented Programming ◽  
Specific Language ◽  
Design Issue ◽  
Language Constructs ◽  
Join Point

The specification of join point selections (also known as "pointcuts") is a major design issue in Aspect-Oriented Software Development. Aspect-oriented systems generally provide specific language constructs (subsumed by the term "pointcut language") for specifying such a join point selection. Pointcut languages differ widely with respect to their syntax and semantics. Consequently, developers familiar with one specific language can hardly benefit from this knowledge when designing and implementing pointcuts in another language. This implies that developers working with different aspect-oriented languages can hardly communicate their design to each other, and knowledge about aspect-oriented design can hardly be transferred among developers developing in different languages. In order to overcome this problem, we present novel specification means based on the UML to represent diverse ways of join point selections — without relying on language-specific syntax and semantics. Instead, the proposed language constructs are able to express join point selections in a variety of different aspect-oriented programming languages.

Sign in / Sign up

Export Citation Format

Share Document