检索结果-内蒙古大学图书馆

Statically safe program generation with SafeGen

SCIENCE OF COMPUTER programming 2011年第5期76卷 376-391页

作者： Huang, Shan Shan Zook, David Smaragdakis, Yannis Georgia Inst Technol Coll Comp Atlanta GA 30332 USA Univ Massachusetts Dept Comp Sci Amherst MA 01003 USA

SafeGen is a meta-programming language for writing statically safe generators of Java programs. If a program generator written in SafeGen passes the checks of the SafeGen compiler, then the generator will only generate well-formed Java programs, for any generator input. In other words, statically checking the generator guarantees the correctness of any generated program, with respect to static checks commonly performed by a conventional compiler (including type safety, existence of a superclass, etc.). To achieve this guarantee, SafeGen supports only language primitives for reflection over an existing well-formed Java program, primitives for creating program fragments, and a restricted set of constructs for iteration, conditional actions, and name generation. SafeGen's static checking algorithm is a combination of traditional type checking for Java, and a series of calls to a theorem prover to check the validity of first-order logical sentences, constructed to represent well-formedness properties of the generated program under all inputs. The approach has worked quite well in our tests, providing proofs for correct generators or pointing out interesting bugs. (C) 2008 Elsevier B.V. All rights reserved.

关键词： meta-programming Domain-specific languages Language extensions

来源：评论

学校读者我要写书评

暂无评论

The metaCoq Project

引用

JOURNAL OF AUTOMATED REASONING 2020年第5期64卷 947-999页

作者： Sozeau, Matthieu Anand, Abhishek Boulier, Simon Cohen, Cyril Forster, Yannick Kunze, Fabian Malecha, Gregory Tabareau, Nicolas Winterhalter, Theo INRIA Gallinette Project Team Nantes France Univ Cote Azur INRIA Nice France Saarland Univ Saarbrucken Germany BedRock Syst Menlo Pk CA USA

The metaCoq project aims to provide a certified meta-programming environment in Coq. It builds on Template-Coq, a plugin for Coq originally implemented by Malecha (Extensible proof engineering in intensional type theory, Harvard University, , 2014), which provided a reifier for Coq terms and global declarations, as represented in the Coq kernel, as well as a denotation command. Recently, it was used in the CertiCoq certified compiler project (Anand et al., in: CoqPL, Paris, France, , 2017), as its front-end language, to derive parametricity properties (Anand and Morrisett, in: CoqPL'18, Los Angeles, CA, USA, 2018). However, the syntax lacked semantics, be it typing semantics or operational semantics, which should reflect, as formal specifications in Coq, the semantics of Coq 's type theory itself. The tool was also rather bare bones, providing only rudimentary quoting and unquoting commands. We generalize it to handle the entire polymorphic calculus of cumulative inductive constructions, as implemented by Coq, including the kernel's declaration structures for definitions and inductives, and implement a monad for general manipulation of Coq 's logical environment. We demonstrate how this setup allows Coq users to define many kinds of general purpose plugins, whose correctness can be readily proved in the system itself, and that can be run efficiently after extraction. We give a few examples of implemented plugins, including a parametricity translation and a certified extraction to call-by-value lambda-calculus. We also advocate the use of metaCoq as a foundation for higher-level tools.

关键词： Proof assistants meta-programming Program certification

来源：评论

学校读者我要写书评

暂无评论

Complex optimization in answer set programming

引用

THEORY AND PRACTICE OF LOGIC programming 2011年第4-5期11卷 821-839页

作者： Gebser, Martin Kaminski, Roland Schaub, Torsten Univ Potsdam Inst Informat Potsdam Germany Simon Fraser Univ Burnaby BC V5A 1S6 Canada Griffith Univ Nathan Qld 4111 Australia

Preference handling and optimization are indispensable means for addressing nontrivial applications in Answer Set programming (ASP). However, their implementation becomes difficult whenever they bring about a significant increase in computational complexity. As a consequence, existing ASP systems do not offer complex optimization capacities, supporting, for instance, inclusion-based minimization or Pareto efficiency. Rather, such complex criteria are typically addressed by resorting to dedicated modeling techniques, like saturation. Unlike the ease of common ASP modeling, however, these techniques are rather involved and hardly usable by ASP laymen. We address this problem by developing a general implementation technique by means of meta-prpogramming, thus reusing existing ASP systems to capture various forms of qualitative preferences among answer sets. In this way, complex preferences and optimization capacities become readily available for ASP applications.

关键词： Answer Set programming Preference Handling Complex optimization meta-programming

来源：评论

学校读者我要写书评

暂无评论

On termination of meta-programs

引用

THEORY AND PRACTICE OF LOGIC programming 2005年第3期5卷 355-390页

作者： Serebrenik, A De Schreye, D TU LaQuSo NL-5600 MB Eindhoven Netherlands Katholieke Univ Leuven Dept Comp Sci B-3001 Heverlee Belgium

The term meta-programming refers to the ability of writing programs that have other programs as data and exploit their semantics. The aim of this paper is presenting a methodology allowing us to perform a correct termination analysis for a broad class of practical meta-interpreters, including negation and performing different tasks during the execution. It is based on combining the power of general orderings, used in proving termination of term-rewrite systems and programs, and on the well-known acceptability condition, used in proving termination of logic programs. The methodology establishes a relationship between the ordering needed to prove termination of the interpreted program and the ordering needed to prove termination of the meta-interpreter together with this interpreted program. If such a relationship is established, termination of one of those implies termination of the other one, i.e. the meta-interpreter preserves termination. Among the meta-interpreters that are analysed correctly are a proof trees constructing meta-interpreter, different kinds of tracers and reasoners.

关键词： termination analysis meta-programming meta-interpreter

来源：评论

学校读者我要写书评

暂无评论

Combining partial evaluation and staged interpretation in the implementation of domain-specific languages

引用

SCIENCE OF COMPUTER programming 2006年第1期62卷 47-65页

作者： Herrmann, Christoph A. Langhammer, Tobias Univ Passau D-94032 Passau Germany Konrad Zuse Zentrum Informat Tech Berlin ZIB Dept Comp Sci Res D-14195 Berlin Germany

We propose a combination of partial evaluation and staged interpretation with metaOCaml for rapid prototyping of domain-specific languages. Interpretation is an easy way to implement such languages. metaOCaml can eliminate the overhead of interpretation at run-time, if the interpreter is written in a staged form, i.e., takes the source program separate from the input data in a first stage. Partial evaluation of the source program with values known at compile time can further improve the target code performance. Additional aggressive optimizations are possible due to the absence of general recursion. Algebraic simplifications can even achieve binding-time improvements during the online partial evaluation. Our approach both saves the application programmer completely from binding-time considerations and exploits staged interpretation with metaOCaml for target code generation. The example domain presented in this paper is image processing, in which the domain-specific language permits the specification of convolution matrices, summations, case distinctions and non-local pixel accesses. All expressions known at compile time are simplified and all remaining expressions are turned into metaOCaml code parts, which are combined to form the compiled application program. The example specifications deal with filtering by convolution and iterations in a series of images for wave effects and temperature distribution. The experimental results show significant speed-ups if online partial evaluation with algebraic simplifications is used for the elimination of interpretation overhead and optimization of code expressions. (c) 2006 Elsevier B.V. All rights reserved.

关键词： binding-time improvement compilation domain-specific languages meta-programming partial evaluation staged interpretation

来源：评论

学校读者我要写书评

暂无评论

Defeasible Reasoning via Datalog not sign

引用

THEORY AND PRACTICE OF LOGIC programming 2023年第5期23卷 986-1028页

作者： Maher, Michael J. Reasoning Res Inst Canberra ACT Australia

We address the problem of compiling defeasible theories to Datalog not sign programs. We prove the correctness of this compilation, for the defeasible logic DL( partial differential (||)), but the techniques we use apply to many other defeasible logics. Structural properties of DL( partial differential (||)) are identified that support efficient implementation and/or approximation of the conclusions of defeasible theories in the logic, compared with other defeasible logics. We also use previously well-studied structural properties of logic programs to adapt to incomplete Datalog not sign implementations.

关键词： defeasible logic program transformation well-founded semantics meta-programming

来源：评论

学校读者我要写书评

暂无评论

On the declarative and procedural semantics of definite metalogic programs

引用

JOURNAL OF LOGIC AND COMPUTATION 1996年第3期6卷 363-407页

作者： Higgins, CP GRIFFITH UNIV SCH COMP & INFORMAT TECHNOL NATHAN QLD 4111 AUSTRALIA

We present declarative and procedural semantics for an amalgamation of object language and metalanguage. We define the class of definite metalogic programs, based on a definite clause language, a binary demonstration predicate, and a naming scheme with both primitive and structured names. The declarative semantics is an extension of the semantics of logic programs dealing with multiple theories and names. The procedural semantics uses a resolution rule and a constructive meta-level to object-level reflection rule.

关键词： amalgamation metalogic meta-programming reflection demo names

来源：评论

学校读者我要写书评

暂无评论

A template system for the efficient compilation of domain abstractions onto reconfigurable computers

引用

JOURNAL OF SYSTEMS ARCHITECTURE 2013年第2期59卷 91-102页

作者： Shafiq, Muhammad Pericas, Miquel Navarro, Nacho Ayguade, Eduard Barcelona Supercomp Ctr Dept Comp Sci Barcelona Spain Univ Politecn Cataluna Dept Comp Architecture E-08028 Barcelona Spain Tokyo Inst Technol Global Sci Informat & Comp Ctr Tokyo Japan

Past research has addressed the issue of using FPGAs as accelerators for HPC systems. Such research has identified that writing low level code for the generation of an efficient, portable and scalable architecture is challenging. We propose to increase the level of abstraction in order to help developers of reconfigurable accelerators deal with these three key issues. Our approach implements domain specific abstractions for FPGA based accelerators using techniques from generic programming. In this paper we explain the main concepts behind our system to Design Accelerators by Template Expansions (DATE). The DATE system can be effectively used for expanding individual kernels of an application and also for the generation of interfaces between various kernels to implement a complete system architecture. We present evaluations for six kernels as examples of individual kernel generation using the proposed system. Our evaluations are mainly intended to provide a proof-of-concept. We also show the usage of the DATE system for integration of various kernels to build a complete system based on a Template Architecture for Reconfigurable Accelerator Designs (TARCAD). (C) 2012 Elsevier B.V. All rights reserved.

关键词： Domain abstractions meta-programming Templates HLL HDL FPGA

来源：评论

学校读者我要写书评

暂无评论

Encoding Abstract Syntax Without Fresh Names

引用

JOURNAL OF AUTOMATED REASONING 2012年第2期49卷 115-140页

作者： Lakin, Matthew R. Pitts, Andrew M. Univ Cambridge Comp Lab Cambridge CB2 3QG England

This paper introduces a variant of nominal abstract syntax in which bindable names are represented by normal meta-variables as opposed to a separate class of globally fresh names. Distinct meta-variables can be instantiated with the same concrete name, which we call aliasing. The possible aliasing patterns are controlled by explicit constraints on the distinctness (freshness) of names. This approach has already been used in the nominal meta-programming language alpha ML. We recap that language and develop a theory of contextual equivalence for it. The central result of the paper is that abstract syntax trees (ASTs) involving binders can be encoded into alpha ML in such a way that alpha-equivalence of ASTs corresponds with contextual equivalence of their encodings. This is novel because the encoding does not rely on the existence of globally fresh names and fresh name generation, which are fundamental to the correctness of the pre-existing encoding of abstract syntax into FreshML.

关键词： meta-programming Alpha-equivalence Nominal abstract syntax

来源：评论

学校读者我要写书评

暂无评论

Specifying and Model Checking Distributed Control Algorithms at meta-level

引用

COMPUTER JOURNAL 2022年第12期65卷 2998-3019页

作者： Ha Thi Thu Doan Ogata, Kazuhiro Univ Freiburg Programming Languages Dept Georges Kohler Allee Geb 079 D-79110 Freiburg Germany Japan Adv Inst Sci & Technol Sch Informat Sci 1-1 Asahidai Nomi Ishikawa 9231292 Japan

This paper proposes an approach to the specification and model checking of a large, important class of distributed algorithms called control algorithms (CAs), which are superimposed on underlying distributed systems (UDSs). The approach is based on rewriting logic by moving from its object level to the meta-level. We introduce the idea of specifying CAs as meta-programs that take the specifications of UDSs and automatically generate the specifications of the UDSs on which the CAs are superimposed (UDS-CAs). Due to many options, such as network topologies, even fixing the number of each kind of entities, such as mobile support stations (MSSs) and mobile hosts (MHs) in a mobile checkpointing algorithm, there are many instances of a UDS. To address the problem, we generate all possible initial states of a UDS for a fixed number of each kind of entities such that some constraints, such as MSSs strongly connected with a wired network, are fulfilled and conduct model checking for each of the initial states. We demonstrate the usefulness by reporting on a case study where a counterexample is found for some specific initial states but not for the other initial states, detecting a subtle flaw lurking in a mobile checkpointing algorithm.

关键词： distributed algorithms control algorithms meta-programming formal specification model checking

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：