Sound and Complete Type Inference for a Systems Programming Language

2008 ◽  
pp. 290-306
Author(s):  
Swaroop Sridhar ◽  
Jonathan S. Shapiro ◽  
Scott F. Smith
Keyword(s):  
Programming Language ◽  
Type Inference ◽  
Complete Type ◽  
Systems Programming

scholarly journals The Emulated OCODE Machine for the Support of BCPL

1975 ◽  
Vol 4 (45) ◽  
Author(s):  
Ole Sørensen
Keyword(s):  
Operating System ◽  
Programming Language ◽  
Design Process ◽  
Internal Representation ◽  
The Past ◽  
Future Analysis ◽  
Systems Programming

In the spring of 1973 it was decided to implement the language BCPL on the experimental microprogrammable computer RIKKE-1 being constructed in this department. The language was chosen to be the systems programming language for RlKKE-1, one argurment being the possibility of transferring the Oxford Operating system OS 8 to RIKKE-1. This paper describes the design process for an internal representation of OCODE, the resulting machine, the emulator, and the assembler, and finally there is a discussion of our experiences of running the OCODE machine during the past 8 months. Some future analysis and possible modifications are mentioned.

FIRST-CLASS CONTEXTS IN ML

2000 ◽  
Vol 11 (01) ◽  
pp. 65-87
Author(s):  
MASATOMO HASHIMOTO
Keyword(s):  
Programming Language ◽  
Operational Semantics ◽  
Type System ◽  
Type Inference ◽  
Inference Algorithm ◽  
Hole Filling ◽  
Dynamic Binding ◽  
Polymorphic Type ◽  
Open Program ◽  
Program Modules

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.

scholarly journals Type Reconstruction for Type Classes

1995 ◽  
Vol 5 (2) ◽  
pp. 201-224 ◽  
Author(s):  
Tobias Nipkow ◽  
Christian Prehofer
Keyword(s):  
Programming Language ◽  
Functional Programming ◽  
Type Inference ◽  
Constraint Solving ◽  
Simple Type ◽  
Inference Problem ◽  
Unification Algorithm ◽  
Type Classes ◽  
Type Reconstruction ◽  
Inference Systems

AbstractWe study the type inference problem for a system with type classes as in the functional programming language Haskell. Type classes are an extension of ML-style polymorphism with overloading. We generalize Milner's work on polymorphism by introducing a separate context constraining the type variables in a typing judgement. This leads to simple type inference systems and algorithms which closely resemble those for ML. In particular, we present a new unification algorithm which is an extension of syntactic unification with constraint solving. The existence of principal types follows from an analysis of this unification algorithm.

Static Type Inference for a First-Order Declarative Visual Programming Language with Inheritance

2000 ◽  
Vol 11 (2) ◽  
pp. 191-235 ◽  
Author(s):  
REBECCA WALPOLE DJANG ◽  
MARGARET M. BURNETT ◽  
ROGER D. CHEN
Keyword(s):  
Programming Language ◽  
Visual Programming ◽  
Type Inference ◽  
First Order ◽  
Visual Programming Language

scholarly journals Gobra: Modular Specification and Verification of Go Programs

2021 ◽  
pp. 367-379
Author(s):  
Felix A. Wolf ◽  
Linard Arquint ◽  
Martin Clochard ◽  
Wytse Oortwijn ◽  
João C. Pereira ◽  
...  
Keyword(s):  
Distributed Systems ◽  
Programming Language ◽  
Message Passing ◽  
Safety Data ◽  
Separation Logic ◽  
Data Race ◽  
Static Verification ◽  
Crash Safety ◽  
Concurrent And Distributed Systems ◽  
Systems Programming

AbstractGo is an increasingly-popular systems programming language targeting, especially, concurrent and distributed systems. Go differentiates itself from other imperative languages by offering structural subtyping and lightweight concurrency through goroutines with message-passing communication. This combination of features poses interesting challenges for static verification, most prominently the combination of a mutable heap and advanced concurrency primitives.We present Gobra, a modular, deductive program verifier for Go that proves memory safety, crash safety, data-race freedom, and user-provided specifications. Gobra is based on separation logic and supports a large subset of Go. Its implementation translates an annotated Go program into the Viper intermediate verification language and uses an existing SMT-based verification backend to compute and discharge proof obligations.

Sign in / Sign up

Export Citation Format

Share Document