scholarly journals Lolisa: Formal Syntax and Semantics for a Subset of the Solidity Programming Language in Mathematical Tool Coq

2020 ◽  
Vol 2020 ◽  
pp. 1-15
Author(s):  
Zheng Yang ◽  
Hang Lei
Keyword(s):  
Programming Languages ◽  
Programming Language ◽  
Type System ◽  
General Purpose ◽  
Mathematical Tool ◽  
Smart Contracts ◽  
Large Subset ◽  
Formal Syntax ◽  
Emerging Issues ◽  
Line Correspondence

The security of blockchain smart contracts is one of the most emerging issues of the greatest interest for researchers. This article presents an intermediate specification language for the formal verification of Ethereum-based smart contract in Coq, denoted as Lolisa. The formal syntax and semantics of Lolisa contain a large subset of the Solidity programming language developed for the Ethereum blockchain platform. To enhance type safety, the formal syntax of Lolisa adopts a stronger static type system than Solidity. In addition, Lolisa includes a large subset of Solidity syntax components as well as general-purpose programming language features. Therefore, Solidity programs can be directly translated into Lolisa with line-by-line correspondence. Lolisa is inherently generalizable and can be extended to express other programming languages. Finally, the syntax and semantics of Lolisa have been encapsulated as an interpreter in mathematical tool Coq. Hence, smart contracts written in Lolisa can be symbolically executed and verified in Coq.

scholarly journals Featherweight generic confinement

2006 ◽  
Vol 16 (6) ◽  
pp. 793-811 ◽  
Author(s):  
ALEX POTANIN ◽  
JAMES NOBLE ◽  
DAVE CLARKE ◽  
ROBERT BIDDLE
Keyword(s):  
Programming Languages ◽  
Ad Hoc ◽  
Type System ◽  
Type Systems ◽  
General Purpose ◽  
Ownership Type ◽  
Essential Change ◽  
Polymorphic Type ◽  
Syntactic Restrictions

Existing approaches to object encapsulation either rely on ad hoc syntactic restrictions or require the use of specialised type systems. Syntactic restrictions are difficult to scale and to prove correct, while specialised type systems require extensive changes to programming languages. We demonstrate that confinement can be enforced cheaply in Featherweight Generic Java, with no essential change to the underlying language or type system. This result demonstrates that polymorphic type parameters can simultaneously act as ownership parameters and should facilitate the adoption of confinement and ownership type systems in general-purpose programming languages.

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 Deep Reinforcement Learning for Syntactic Error Repair in Student Programs

2019 ◽  
Vol 33 ◽  
pp. 930-937 ◽  
Author(s):  
Rahul Gupta ◽  
Aditya Kanade ◽  
Shirish Shevade
Keyword(s):  
Reinforcement Learning ◽  
Programming Languages ◽  
Programming Language ◽  
Online Course ◽  
Program Text ◽  
Neural Machine Translation ◽  
C Programs ◽  
Massive Open Online Course ◽  
Formal Syntax ◽  
Error Repair

Novice programmers often struggle with the formal syntax of programming languages. In the traditional classroom setting, they can make progress with the help of real time feedback from their instructors which is often impossible to get in the massive open online course (MOOC) setting. Syntactic error repair techniques have huge potential to assist them at scale. Towards this, we design a novel programming language correction framework amenable to reinforcement learning. The framework allows an agent to mimic human actions for text navigation and editing. We demonstrate that the agent can be trained through self-exploration directly from the raw input, that is, program text itself, without either supervision or any prior knowledge of the formal syntax of the programming language. We evaluate our technique on a publicly available dataset containing 6975 erroneous C programs with typographic errors, written by students during an introductory programming course. Our technique fixes 1699 (24.4%) programs completely and 1310 (18.8%) program partially, outperforming DeepFix, a state-of-the-art syntactic error repair technique, which uses a fully supervised neural machine translation approach.

scholarly journals Interval-Based Simulation of Zélus IVPs using DynIbex

2020 ◽  
Author(s):  
Jason Brown ◽  
François Pessaux
Keyword(s):  
Dynamical Systems ◽  
Programming Languages ◽  
Programming Language ◽  
Continuous Time ◽  
General Purpose ◽  
Complex Task ◽  
Integration Methods

Modeling continuous-time dynamical systems is a complex task. Fortunately some dedicated programming languages exist to ease this work. Zélus is one such language that generates a simulation executable which can be used to study the behavior of the modeled system. However, such simulations cannot handle uncertainties on some parameters of the system. This makes it necessary to run multiple simulations to check that the system fulfills particular requirements (safety for instance) for all the values in the uncertainty ranges. Interval-based guaranteed integration methods provide a solution to this problem. The DynIbex library provides such methods but it requires a manual encoding of the system in a general purpose programming language (C++). This article presents an extension of the Zélus compiler to generate interval-based guaranteed simulations of IVPs using DynIbex. This extension is conservative since it does not break the existing compilation workflow.

scholarly journals All Smart Contracts Are Ambiguous

2019 ◽  
Author(s):  
James Grimmelmann
Keyword(s):  
Computer Program ◽  
Programming Languages ◽  
Programming Language ◽  
Social Process ◽  
Smart Contracts ◽  
Natural Languages ◽  
Virtual Currency ◽  
Smart Contract

Smart contracts are written in programming languages rather than in natural languages. This might seem to insulate them from ambiguity, because the meaning of a program is determined by technical facts rather than by social ones. It does not. Smart contracts can be ambiguous, too, because technical facts depend on socially determined ones. To give meaning to a computer program, a community of programmers and users must agree on the semantics of the programming language in which it is written. This is a social process, and a review of some famous controversies involving blockchains and smart contracts shows that it regularly creates serious ambiguities. In the most famous case, The DAO hack, more than $150 million in virtual currency turned on the contested semantics of a blockchain-based smart-contract programming language.

Language-agnostic integrated queries in a managed polyglot runtime

2021 ◽  
Vol 14 (8) ◽  
pp. 1414-1426
Author(s):  
Filippo Schiavio ◽  
Daniele Bonetta ◽  
Walter Binder
Keyword(s):  
Programming Languages ◽  
Type System ◽  
Database Systems ◽  
General Purpose ◽  
Multiple Sources ◽  
Server Side ◽  
Query Engine ◽  
Combining Data ◽  
Dynamic Languages ◽  
Memory Object

Language-integrated query (LINQ) frameworks offer a convenient programming abstraction for processing in-memory collections of data, allowing developers to concisely express declarative queries using general-purpose programming languages. Existing LINQ frameworks rely on the well-defined type system of statically-typed languages such as C # or Java to perform query compilation and execution. As a consequence of this design, they do not support dynamic languages such as Python, R, or JavaScript. Such languages are however very popular among data scientists, who would certainly benefit from LINQ frameworks in data analytics applications. In this work we bridge the gap between dynamic languages and LINQ frameworks. We introduce DynQ, a novel query engine designed for dynamic languages. DynQ is language-agnostic, since it is able to execute SQL queries in a polyglot language runtime. Moreover, DynQ can execute queries combining data from multiple sources, namely in-memory object collections as well as on-file data and external database systems. Our evaluation of DynQ shows performance comparable with equivalent hand-optimized code, and in line with common data-processing libraries and embedded databases, making DynQ an appealing query engine for standalone analytics applications and for data-intensive server-side workloads.

scholarly journals Type Safe Metadata Combining

2017 ◽  
Vol 10 (2) ◽  
pp. 97
Author(s):  
Mikus Vanags ◽  
Rudite Cevere
Keyword(s):  
Programming Languages ◽  
Programming Language ◽  
Type System ◽  
Data Abstraction ◽  
Class Member ◽  
Database Querying ◽  
Type Safety ◽  
Abstraction Layer ◽  
Information Type ◽  
Type Information

Type safety is an important property of any type system. Modern programming languages support different mechanisms to work in type safe manner, e.g., properties, methods, events, attributes (annotations) and other structures. Some programming languages allow access to metadata: type information, type member information and information about applied attributes. But none of the existing mainstream programming languages which support reflection provides fully type safe metadata combining mechanism built in the programming language. Combining of metadata means a class member metadata combining with data, type metadata and constraints. Existing solutions provide no or limited type safe metadata combining mechanism; they are complex and processed at runtime, which by definition is not built-in type-safe metadata combining. Problem can be solved by introducing syntax and methods for type safe metadata combining so that, metadata could be processed at compile time in a fully type safe way. Common metadata combining use cases are data abstraction layer creation and database querying.

scholarly journals SpecTest: Specification-Based Compiler Testing

2021 ◽  
pp. 269-291
Author(s):  
Richard Schumi ◽  
Jun Sun
Keyword(s):  
Programming Languages ◽  
Programming Language ◽  
General Purpose ◽  
Test Coverage ◽  
Domain Specific ◽  
Test Oracle ◽  
Coverage Criterion ◽  
Language Semantics ◽  
Compiler Testing ◽  
Semantic Errors

AbstractCompilers are error-prone due to their high complexity. They are relevant for not only general purpose programming languages, but also for many domain specific languages. Bugs in compilers can potentially render all programs at risk. It is thus crucial that compilers are systematically tested, if not verified. Recently, a number of efforts have been made to formalise and standardise programming language semantics, which can be applied to verify the correctness of the respective compilers. In this work, we present a novel specification-based testing method named SpecTest to better utilise these semantics for testing. By applying an executable semantics as test oracle, SpecTest can discover deep semantic errors in compilers. Compared to existing approaches, SpecTest is built upon a novel test coverage criterion called semantic coverage which brings together mutation testing and fuzzing to specifically target less tested language features. We apply SpecTest to systematically test two compilers, i.e., the Java compiler and the Solidity compiler. SpecTest improves the semantic coverage of both compilers considerably and reveals multiple previously unknown bugs.

Extending C and FORTRAN for Design Automation

1995 ◽  
Vol 117 (3) ◽  
pp. 390-395 ◽  
Author(s):  
H. H. Cheng
Keyword(s):  
Programming Languages ◽  
Programming Language ◽  
Systems Engineering ◽  
Design Automation ◽  
Mechanical Systems ◽  
General Purpose ◽  
Software Packages ◽  
Fortran 77

The CH programming language is designed to be a superset of C. CH bridges the gap between C and FORTRAN; it encompasses all the programming capabilities of FORTRAN 77 and consists of features of many other programming languages and software packages. Unlike other general-purpose programming languages, CH is designed to be especially suitable for applications in mechanical systems engineering. Because of our research interests, many programming features in CH have been implemented for design automation, although they are useful in other applications as well. In this paper we will describe these new programming features for design automation, as they are currently implemented in CH in comparison with C and FORTRAN 77.

Sign in / Sign up

Export Citation Format

Share Document