scholarly journals A Brief Introduction to the PVS2C Code Generator

10.29007/v7k2 ◽  
2018 ◽  
Author(s):  
Natarajan Shankar
Keyword(s):  
Higher Order ◽  
Specification Language ◽  
Functional Language ◽  
Data Types ◽  
Code Generator ◽  
Numeric Data ◽  
Recursive Data

We present a brief tutorial on the PVS2C code generator for producing C code from an applicative fragment of the PVS specification language. This fragment roughly corresponds to a self-contained functional language. The tutorial covers the generation of C code for numeric data types and associated operations, arrays, recursive data types, and higher- order operations.

The bologna optimal higher-order machine

1996 ◽  
Vol 6 (6) ◽  
pp. 763-810 ◽  
Author(s):  
Andrea Asperti ◽  
Cecilia Giovannetti ◽  
Andrea Naletto
Keyword(s):  
Higher Order ◽  
Reduction Technique ◽  
Large Set ◽  
Functional Language ◽  
Data Types ◽  
Garbage Collector ◽  
Source Language ◽  
The Core ◽  
General Architecture ◽  
Optimal Graph

AbstractThe Bologna Optimal Higher-order Machine (BOHM) is a prototype implementation of the core of a functional language based on (a variant of) Lamping's optimal graph reduction technique (Lamping, 1990; Gonthier et al., 1992a; Asperti, 1994). The source language is a sugared λ-calculus enriched with booleans, integers, lists and basic operations on these data types (following the guidelines of Interaction Systems – Asperti and Laneve (1993b, 1994), Laneve (1993)). In this paper, we shall describe BOHM's general architecture (comprising the garbage collector), and give a large set of benchmarks and experimental results.

A system of constructor classes: overloading and implicit higher-order polymorphism

1995 ◽  
Vol 5 (1) ◽  
pp. 1-35 ◽  
Author(s):  
Mark P. Jones
Keyword(s):  
Type System ◽  
Type Systems ◽  
Natural Generalization ◽  
Higher Order ◽  
Functional Language ◽  
Effective Algorithm ◽  
Prototype Implementation ◽  
Type Classes

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.

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.

scholarly journals EVL: A Typed Higher-order Functional Language for Events

2020 ◽  
Vol 351 ◽  
pp. 3-23
Author(s):  
Sandra Alves ◽  
Maribel Fernández ◽  
Miguel Ramos
Keyword(s):  
Higher Order ◽  
Functional Language

scholarly journals Functional geometry of protein interactomes

2019 ◽  
Vol 35 (19) ◽  
pp. 3727-3734 ◽  
Author(s):  
Noël Malod-Dognin ◽  
Nataša Pržulj
Keyword(s):  
Functional Organization ◽  
Protein Complexes ◽  
Simplicial Complexes ◽  
Higher Order ◽  
Biological Information ◽  
Supplementary Information ◽  
Data Types ◽  
Ppi Networks ◽  
Functional Geometry ◽  
Better Than

Abstract Motivation Protein–protein interactions (PPIs) are usually modeled as networks. These networks have extensively been studied using graphlets, small induced subgraphs capturing the local wiring patterns around nodes in networks. They revealed that proteins involved in similar functions tend to be similarly wired. However, such simple models can only represent pairwise relationships and cannot fully capture the higher-order organization of protein interactomes, including protein complexes. Results To model the multi-scale organization of these complex biological systems, we utilize simplicial complexes from computational geometry. The question is how to mine these new representations of protein interactomes to reveal additional biological information. To address this, we define simplets, a generalization of graphlets to simplicial complexes. By using simplets, we define a sensitive measure of similarity between simplicial complex representations that allows for clustering them according to their data types better than clustering them by using other state-of-the-art measures, e.g. spectral distance, or facet distribution distance. We model human and baker’s yeast protein interactomes as simplicial complexes that capture PPIs and protein complexes as simplices. On these models, we show that our newly introduced simplet-based methods cluster proteins by function better than the clustering methods that use the standard PPI networks, uncovering the new underlying functional organization of the cell. We demonstrate the existence of the functional geometry in the protein interactome data and the superiority of our simplet-based methods to effectively mine for new biological information hidden in the complexity of the higher-order organization of protein interactomes. Availability and implementation Codes and datasets are freely available at http://www0.cs.ucl.ac.uk/staff/natasa/Simplets/. Supplementary information Supplementary data are available at Bioinformatics online.

Sign in / Sign up

Export Citation Format

Share Document