Mathematical Semantics for Higher Order Programming Languages.

1980 ◽  
Author(s):  
Luis E. Sanchis
Keyword(s):  
Programming Languages ◽  
Higher Order ◽  
Mathematical Semantics

scholarly journals Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs

10.29007/jqtz ◽  
2018 ◽  
Author(s):  
Nada Habli ◽  
Amy P. Felty
Keyword(s):  
Programming Languages ◽  
Automatic Generation ◽  
Higher Order ◽  
Specification Language ◽  
Proof Assistants ◽  
Abstract Syntax ◽  
Formal Systems ◽  
Ongoing Work ◽  
General Specification ◽  
Automated Proof

We describe ongoing work on building an environment to support reasoning in proof assistants that represent formal systems using higher-order abstract syntax (HOAS). We use a simple and general specification language whose syntax supports HOAS. Using this language, we can encode the syntax and inference rules of a variety of formal systems, such as programming languages and logics. We describe our tool, implemented in OCaml, which parses this syntax, and translates it to a Coq library that includes definitions and hints for aiding automated proof in the Hybrid system. Hybrid itself is implemented in Coq, and designed specifically to reason about such formal systems. Given an input specification, the library that is automatically generated by our tool imports the general Hybrid library and adds definitions and hints for aiding automated proof in Hybrid about the specific programming language or logic defined in the specification. This work is part of a larger project to compare reasoning in systems supporting HOAS. Our current work focuses on Hybrid, Abella, Twelf, and Beluga, and the specification language is designed to be general enough to allow the automatic generation of libraries for all of these systems from a single specification.

Principal signatures for higher-order program modules

1994 ◽  
Vol 4 (3) ◽  
pp. 285-335 ◽  
Author(s):  
Mads Tofte
Keyword(s):  
Programming Languages ◽  
Functional Programming ◽  
Operational Semantics ◽  
Higher Order ◽  
Principal Type ◽  
Functional Programming Languages ◽  
Standard Ml ◽  
Static Semantics ◽  
Program Modules

AbstractIn this paper we present a language for programming with higher-order modules. The language HML is based on Standard ML in that it provides structures, signatures and functors. In HML, functors can be declared inside structures and specified inside signatures; this is not possible in Standard ML. We present an operational semantics for the static semantics of HML signature expressions, with particular emphasis on the handling of sharing. As a justification for the semantics, we prove a theorem about the existence of principal signatures. This result is closely related to the existence of principal type schemes for functional programming languages with polymorphism.

A Framework for Object-Oriented Data Mining Based on Higher-Order Logic Programming

2013 ◽  
Vol 420 ◽  
pp. 325-332 ◽  
Author(s):  
Zhi Ping Zhang ◽  
Lin Na Li ◽  
Li Jun Wang ◽  
Hai Yan Yu
Keyword(s):  
Data Mining ◽  
Logic Programming ◽  
Programming Languages ◽  
Inductive Logic ◽  
Object Oriented ◽  
Higher Order ◽  
Order Logic ◽  
Higher Order Logic ◽  
Representation Formalism ◽  
Object Oriented Database

Data mining discovers knowledge and useful information from large amounts of data stored in databases. With the increasing popularity of object-oriented database system in advanced database applications, it is significantly important to study the data mining methods for object-oriented database. This paper proposes that higher-order logic programming languages and techniques is very suitable for object-oriented data mining, and presents a framework for object-oriented data mining based on higher-order logic programming. Such a framework is inductive logic programming which adopts higher-order logic programming language Escher as knowledge representation formalism. In addition, Escher is a generalization of the attribute-value representation, thus many higher-order logic learners under this framework can be upgraded directly from corresponding propositional learners.

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 On the Versatility of Open Logical Relations

2020 ◽  
pp. 56-83 ◽  
Author(s):  
Gilles Barthe ◽  
Raphaëlle Crubillé ◽  
Ugo Dal Lago ◽  
Francesco Gavazzo
Keyword(s):  
Programming Languages ◽  
Automatic Differentiation ◽  
Type System ◽  
Order Type ◽  
Higher Order ◽  
Base Case ◽  
Logical Relation ◽  
First Order ◽  
Differentiable Functions ◽  
The One

AbstractLogical relations are one among the most powerful techniques in the theory of programming languages, and have been used extensively for proving properties of a variety of higher-order calculi. However, there are properties that cannot be immediately proved by means of logical relations, for instance program continuity and differentiability in higher-order languages extended with real-valued functions. Informally, the problem stems from the fact that these properties are naturally expressed on terms of non-ground type (or, equivalently, on open terms of base type), and there is no apparent good definition for a base case (i.e. for closed terms of ground types). To overcome this issue, we study a generalization of the concept of a logical relation, called open logical relation, and prove that it can be fruitfully applied in several contexts in which the property of interest is about expressions of first-order type. Our setting is a simply-typed $$\lambda $$ λ -calculus enriched with real numbers and real-valued first-order functions from a given set, such as the one of continuous or differentiable functions. We first prove a containment theorem stating that for any collection of real-valued first-order functions including projection functions and closed under function composition, any well-typed term of first-order type denotes a function belonging to that collection. Then, we show by way of open logical relations the correctness of the core of a recently published algorithm for forward automatic differentiation. Finally, we define a refinement-based type system for local continuity in an extension of our calculus with conditionals, and prove the soundness of the type system using open logical relations.

A calculus with polymorphic and polyvariant flow types

2002 ◽  
Vol 12 (3) ◽  
pp. 183-227 ◽  
Author(s):  
J. B. WELLS ◽  
ALLYN DIMOCK ◽  
ROBERT MULLER ◽  
FRANKLYN TURBAK
Keyword(s):  
Programming Languages ◽  
Data Flow ◽  
Higher Order ◽  
Program Transformations ◽  
Optimizing Compilers ◽  
Intermediate Language ◽  
Program Representation ◽  
Key Innovation ◽  
Data Representations ◽  
Flow Information

We present λCIL, a typed λ-calculus which serves as the foundation for a typed intermediate language for optimizing compilers for higher-order polymorphic programming languages. The key innovation of λCIL is a novel formulation of intersection and union types and flow labels on both terms and types. These flow types can encode polyvariant control and data flow information within a polymorphically typed program representation. Flow types can guide a compiler in generating customized data representations in a strongly typed setting. Since λCIL enjoys confluence, standardization, and subject reduction properties, it is a valuable tool for reasoning about programs and program transformations.

Sign in / Sign up

Export Citation Format

Share Document