scholarly journals Type-Directed Partial Evaluation

1995 ◽  
Vol 24 (494) ◽  
Author(s):  
Olivier Danvy
Keyword(s):  
Programming Languages ◽  
Code Generation ◽  
Compiler Optimization ◽  
Partial Evaluation ◽  
Lambda Calculus ◽  
Denotational Semantics ◽  
Compiler Generation ◽  
Environment Type ◽  
Symbolic Evaluation ◽  
Specialized Program

<p>We present a strikingly simple partial evaluator, that is type-directed and reifies a compiled program into the text of a residual, specialized program. Our partial evaluator is concise (a few lines) and it handles the flagship examples of offline monovariant partial evaluation. Its source programs are constrained in two ways: they must be closed and monomorphically typable. Thus dynamic free variables need to be factored out in a ``dynamic initial environment´´. Type-directed partial evaluation uses no symbolic evaluation for specialization, and naturally processes static computational effects.</p><p>Our partial evaluator is the part of an offline partial evaluator that residualizes static values in dynamic contexts. Its restriction to the simply typed lambda-calculus coincides with Berger and Schwichtenberg's ``inverse of the evaluation functional´´ (LICS'91), which is an instance of normalization in a logical setting. As such, type-directed partial evaluation essentially achieves lambda-calculus normalization. We extend it to produce specialized programs that are recursive and that use disjoint sums and computational effects. We also analyze its limitations: foremost, it does not handle inductive types.</p><p>This paper therefore bridges partial evaluation and lambda-calculus normalization through higher-order abstract syntax, and touches upon parametricity, proof theory, and type theory (including subtyping and coercions), compiler optimization, and run-time code generation (including decompilation). It also offers a simple solution to denotational semantics-based compilation and compiler generation.</p><p>Proceedings of POPL96, the 1996 ACM Symposium on Principles of Programming Languages (to appear).</p>

scholarly journals Compiler Generation from Denotational Semantics

1980 ◽  
Vol 9 (113) ◽  
Author(s):  
Neil D. Jones
Keyword(s):  
Programming Languages ◽  
State Transition ◽  
Lambda Calculus ◽  
Denotational Semantics ◽  
Optimization Methods ◽  
Compiler Generation ◽  
Syntax Rule ◽  
Language L ◽  
Algebraic Framework ◽  
Efficient Code

<p>A methodology is described for generating provably correct compilers from denotational definitions of programming languages. An application is given to produce compilers into STM code (an STM or state transition machine is a flow-chart-like program, low-level enough to be translated into efficient code on conventional computers). First, a compiler phi: LAMC -&gt; STM from a lambda calculus dialect is defined. Any denotational definition DD of language L defines a map DD': L -&gt; LAMC, so DD'_circle phi compiles L into STM code. Correctness follows from the correctness of phi.</p><p>The algebraic framework of Morris, ADJ, etc. is used. The set of STMs is given an algebraic structure so any DD'_circ phi may be specified by giving a derived operator on STM for each syntax rule of L.</p><p>This approach yields quite redundant object programs, so the paper ends by describing two flow analytic optimization methods. The first analyzes an already-produced STM to obtain information about its runtime behaviour which is used to optimize the STM. The second analyzes the generated compiling scheme to determine runtime properties of object programs in general which a compiler can use to produce less redundant STMs.</p>

scholarly journals Denotational semantics of recursive types in synthetic guarded domain theory

2018 ◽  
Vol 29 (3) ◽  
pp. 465-510 ◽  
Author(s):  
RASMUS E. MØGELBERG ◽  
MARCO PAVIOTTI
Keyword(s):  
Programming Languages ◽  
Type Theory ◽  
Operational Semantics ◽  
Lambda Calculus ◽  
Denotational Semantics ◽  
Domain Theory ◽  
Logical Relation ◽  
Dependent Type Theory ◽  
Semantics Of Programming Languages ◽  
Dependent Type

Just like any other branch of mathematics, denotational semantics of programming languages should be formalised in type theory, but adapting traditional domain theoretic semantics, as originally formulated in classical set theory to type theory has proven challenging. This paper is part of a project on formulating denotational semantics in type theories with guarded recursion. This should have the benefit of not only giving simpler semantics and proofs of properties such as adequacy, but also hopefully in the future to scale to languages with advanced features, such as general references, outside the reach of traditional domain theoretic techniques.Working inGuarded Dependent Type Theory(GDTT), we develop denotational semantics for Fixed Point Calculus (FPC), the simply typed lambda calculus extended with recursive types, modelling the recursive types of FPC using the guarded recursive types ofGDTT. We prove soundness and computational adequacy of the model inGDTTusing a logical relation between syntax and semantics constructed also using guarded recursive types. The denotational semantics is intensional in the sense that it counts the number of unfold-fold reductions needed to compute the value of a term, but we construct a relation relating the denotations of extensionally equal terms, i.e., pairs of terms that compute the same value in a different number of steps. Finally, we show how the denotational semantics of terms can be executed inside type theory and prove that executing the denotation of a boolean term computes the same value as the operational semantics of FPC.

scholarly journals Automated Source Code Generation and Auto-Completion Using Deep Learning: Comparing and Discussing Current Language Model-Related Approaches

AI ◽  
2021 ◽  
Vol 2 (1) ◽  
pp. 1-16
Author(s):  
Juan Cruz-Benito ◽  
Sanjay Vishwakarma ◽  
Francisco Martin-Fernandez ◽  
Ismael Faro
Keyword(s):  
Deep Learning ◽  
Learning Community ◽  
Programming Languages ◽  
Language Processing ◽  
Code Generation ◽  
Language Model ◽  
Language Models ◽  
Stochastic Gradient Descent ◽  
Network Architectures ◽  
Learning Architectures

In recent years, the use of deep learning in language models has gained much attention. Some research projects claim that they can generate text that can be interpreted as human writing, enabling new possibilities in many application areas. Among the different areas related to language processing, one of the most notable in applying this type of modeling is programming languages. For years, the machine learning community has been researching this software engineering area, pursuing goals like applying different approaches to auto-complete, generate, fix, or evaluate code programmed by humans. Considering the increasing popularity of the deep learning-enabled language models approach, we found a lack of empirical papers that compare different deep learning architectures to create and use language models based on programming code. This paper compares different neural network architectures like Average Stochastic Gradient Descent (ASGD) Weight-Dropped LSTMs (AWD-LSTMs), AWD-Quasi-Recurrent Neural Networks (QRNNs), and Transformer while using transfer learning and different forms of tokenization to see how they behave in building language models using a Python dataset for code generation and filling mask tasks. Considering the results, we discuss each approach’s different strengths and weaknesses and what gaps we found to evaluate the language models or to apply them in a real programming context.

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 An Abstract Contract Theory for Programs with Procedures

2021 ◽  
pp. 152-171
Author(s):  
Christian Lidström ◽  
Dilian Gurov
Keyword(s):  
Programming Languages ◽  
Contract Theory ◽  
Denotational Semantics ◽  
The Other ◽  
Hoare Logic ◽  
Basic Building Block ◽  
Sequential Programming ◽  
Modular Verification ◽  
The One ◽  
Meta Theory

AbstractWhen developing complex software and systems, contracts provide a means for controlling the complexity by dividing the responsibilities among the components of the system in a hierarchical fashion. In specific application areas, dedicated contract theories formalise the notion of contract and the operations on contracts in a manner that supports best the development of systems in that area. At the other end, contract meta-theories attempt to provide a systematic view on the various contract theories by axiomatising their desired properties. However, there exists a noticeable gap between the most well-known contract meta-theory of Benveniste et al. [5], which focuses on the design of embedded and cyber-physical systems, and the established way of using contracts when developing general software, following Meyer’s design-by-contract methodology [18]. At the core of this gap appears to be the notion of procedure: while it is a central unit of composition in software development, the meta-theory does not suggest an obvious way of treating procedures as components.In this paper, we provide a first step towards a contract theory that takes procedures as the basic building block, and is at the same time an instantiation of the meta-theory. To this end, we propose an abstract contract theory for sequential programming languages with procedures, based on denotational semantics. We show that, on the one hand, the specification of contracts of procedures in Hoare logic, and their procedure-modular verification, can be cast naturally in the framework of our abstract contract theory. On the other hand, we also show our contract theory to fulfil the axioms of the meta-theory. In this way, we give further evidence for the utility of the meta-theory, and prepare the ground for combining our instantiation with other, already existing instantiations.

Documentation Methods for Visual Languages

2011 ◽  
pp. 436-454
Author(s):  
Eduardo Costa ◽  
Alexandre Grings ◽  
Marcus Vinicius dos Santos
Keyword(s):  
Programming Languages ◽  
Denotational Semantics ◽  
Visual Programming ◽  
Visual Adaptation ◽  
Visual Languages

Many people argue that Visual Programming languages are self-documenting. This article points out that there is no such thing as a self-documenting language. Besides this, many popular methods used to document programs written in other languages do not suit Visual Languages perfectly, and need some tailoring. Therefore, the authors propose a visual adaptation of the dataflow method of documentation. They also present versions of instantiated documentation and denotational semantics applied to visual languages. Finally, they present a Prolog based complete example of documentation.

Sign in / Sign up

Export Citation Format

Share Document