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 POPLMark reloaded: Mechanizing proofs by logical relations

2019 ◽  
Vol 29 ◽  
Author(s):  
ANDREAS ABEL ◽  
GUILLAUME ALLAIS ◽  
ALIYA HAMEER ◽  
BRIGITTE PIENTKA ◽  
ALBERTO MOMIGLIANO ◽  
...  
Keyword(s):  
Programming Languages ◽  
State Of The Art ◽  
General Purpose ◽  
Higher Order ◽  
Lessons Learned ◽  
Benchmark Problems ◽  
Proof Assistants ◽  
Abstract Syntax ◽  
The Masses

Abstract We propose a new collection of benchmark problems in mechanizing the metatheory of programming languages, in order to compare and push the state of the art of proof assistants. In particular, we focus on proofs using logical relations (LRs) and propose establishing strong normalization of a simply typed calculus with a proof by Kripke-style LRs as a benchmark. We give a modern view of this well-understood problem by formulating our LR on well-typed terms. Using this case study, we share some of the lessons learned tackling this problem in different dependently typed proof environments. In particular, we consider the mechanization in Beluga, a proof environment that supports higher-order abstract syntax encodings and contrast it to the development and strategies used in general-purpose proof assistants such as Coq and Agda. The goal of this paper is to engage the community in discussions on what support in proof environments is needed to truly bring mechanized metatheory to the masses and engage said community in the crafting of future benchmarks.

scholarly journals GERADOR DE CÓDIGOS PARA O DESENVOLVIMENTO DE APLICAÇÕES WEB A PARTIR DA MODELAGEM ENTIDADE-RELACIONAMENTO

e-xacta ◽  
2016 ◽  
Vol 9 (1) ◽  
pp. 37
Author(s):  
Cristiano Martins Monteiro ◽  
Flavianne Braga Campos de Lima ◽  
Carlos Renato Storck
Keyword(s):  
Programming Languages ◽  
Code Generation ◽  
Design Pattern ◽  
Design Patterns ◽  
Source Code ◽  
Automatic Generation ◽  
Code Generator ◽  
Routine Tasks ◽  
Entity Relationship ◽  
Web Systems

<p>A geração automática de código-fonte é uma prática adotada no desenvolvimento de softwares para agilizar, facilitar e padronizar a implementação dos projetos. Embora seja uma prática comum nas fábricas de software, não se conhece uma ferramenta que permita escolher o padrão de projeto a ser usado. O objetivo principal deste trabalho é apresentar um gerador de códigos para o desenvolvimento de sistemas Web a partir de uma modelagem entidade-relacionamento, uma linguagem de programação e um padrão de projeto determinados pelo usuário. Os objetivos específicos são propor uma arquitetura do sistema capaz de adequar e reaproveitar diferentes padrões de projeto, linguagens de programação e projetos cadastrados; permitir que o usuário cadastre, altere, exclua, importe e exporte um projeto; e gerar automaticamente o seu código-fonte e scripts de banco de dados. Este trabalho se justifica pela importância de reduzir erros de codificação; e evitar perca tempo ao realizar atividades rotineiras de implementação de padrões de projeto. Possibilitando assim, maior dedicação no planejamento das regras de negócios e redução de custos. A ferramenta proposta (GCER) foi desenvolvida em linguagem Java com o uso banco de dados Oracle 11g, e seguindo os padrões DAO e MVC. Os resultados foram avaliados através da geração e compilação de códigos de um projeto para cadastro de veículos. A geração com êxito evidencia a viabilidade da ferramenta proposta para a geração automática de códigos no processo de desenvolvimento de software.</p><p>Abstract</p><p>The automatic generation of source code is a practice adopted in the development of software to streamline, facilitate and standardize the implementation of projects. Although it be a common practice in software factories, it is not known a tool able to choose the design pattern to be used. The main objective of this paper is to present a code generator for the development of Web systems from an entity-relationship modeling, a programming language and a design pattern determined by the user. The specific objectives are to propose a system architecture able to suit and reuse different design patterns, programming languages and saved projects; allow the user to insert, update, delete, import and export a project; and automatically generate the source code and database scripts. This work is justified by the importance to reduce errors of coding; and to avoid waste of time in the development of Web systems performing routine tasks. Allowing, then, a greater dedication in the planning of business rules and the reduction of costs. The tool proposed (GCER) was developed in Java with the database using Oracle 11g, and following the DAO and MVC patterns. The results were evaluated by generating and compiling codes of a project for vehicle registration. The successful code generation demonstrate the feasibility of the proposed tool for the automatic generation of code in the software development process.</p>

scholarly journals Constructive Galois Connections

2019 ◽  
Vol 29 ◽  
Author(s):  
DAVID DARAIS ◽  
DAVID VAN HORN
Keyword(s):  
Programming Languages ◽  
Case Studies ◽  
Functional Programming ◽  
Abstract Interpretation ◽  
Proof Assistants ◽  
Functional Programming Languages ◽  
General Application ◽  
Galois Connections ◽  
Gradual Typing ◽  
Specification And Implementation

AbstractGalois connections are a foundational tool for structuring abstraction in semantics, and their use lies at the heart of the theory of abstract interpretation. Yet, mechanization of Galois connections using proof assistants remains limited to restricted modes of use, preventing their general application in mechanized metatheory and certified programming. This paper presents constructive Galois connections, a variant of Galois connections that is effective both on paper and in proof assistants; is complete with respect to a large subset of classical Galois connections; and enables more general reasoning principles, including the “calculational” style advocated by Cousot. To design constructive Galois connections, we identify a restricted mode of use of classical ones which is both general and amenable to mechanization in dependently typed functional programming languages. Crucial to our metatheory is the addition of monadic structure to Galois connections to control a “specification effect.” Effectful calculations may reason classically, while pure calculations have extractable computational content. Explicitly moving between the worlds of specification and implementation is enabled by our metatheory. To validate our approach, we provide two case studies in mechanizing existing proofs from the literature: the first uses calculational abstract interpretation to design a static analyzer, and the second forms a semantic basis for gradual typing. Both mechanized proofs closely follow their original paper-and-pencil counterparts, employ reasoning principles not captured by previous mechanization approaches, support the extraction of verified algorithms, and are novel.

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.

Sign in / Sign up

Export Citation Format

Share Document