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

10th International Conference on Rigorous State-Based Methods (ABZ)

作者： Armbruester, Julius Koerner, Philipp Heinrich Heine Univ Dusseldorf Fac Math & Nat Sci Dept Comp Sci D-40225 Dusseldorf Germany

ISBN: (纸本)9783031637896;9783031637902

Transforming models based on their textual representation is a cumbersome task. This is particularly the case for Event-B, where the predominant representation is a set of XML files. As a consequence, tool support is lacking, even for minor refactoring operations. The contribution of this paper extends the lisb library with a front and backend based on Event-B. The aim is to bring benefits, that have been demonstrated for classical B, such as an easily transformable data representation of formal specifications as well as creation of custom DSLs and tooling, to Event-B. We see great benefits of such a meta-programming approach for formal specifications and advocate that similar mechanisms will be sensible extensions to the expressiveness of formal methods. Ultimately, our work facilitates language extensions (e.g., re-introducing if-then-else constructs to Event-B which generate multiple events or a proper macro system to avoid code duplication) and tool support (e.g., refactoring tools or automatic refinement).

关键词： B-Method Event-B meta-programming

来源：评论

学校读者我要写书评

暂无评论

A Dependent Type Theory for meta-programming with Intensional Analysis

引用

PROCEEDINGS OF THE ACM ON programming LANGUAGES-PACMPL 2025年第POPL期9卷 416-445页

作者： Hu, Jason Z. S. Pientka, Brigitte McGill Univ Montreal PQ Canada

In this paper, we introduce DELAM, a dependent layered modal type theory which enables meta-programming in Martin-L & ouml;f type theory (MLTT) with recursion principles on open code. DELAM includes three layers: the layer of static syntax objects of MLTT without any computation, the layer of pure MLTT with the computational behaviors, and the meta-programming layer, which extends MLTT with support for quoting an open MLTT code object, composing, and analyzing open code using recursion. We can also execute a code object at the meta-programming layer. The expressive power strictly increases as we move up in a given layer. In particular, while code objects only describe static syntax, we allow computation at the MLTT and meta-programming layer. As a result, DELAM provides a dependently typed foundation for meta-programming that supports both type-safe code generation and code analysis. We prove the weak normalization of DELAM and the decidability of convertibility using Kripke logical relations.

关键词： dependent types logical relations meta-programming intensional analysis modal type theory contextual types

来源：评论

学校读者我要写书评

暂无评论

A Type-Theoretic Framework for Certified meta-programming (Invited Talk Extended Abstract) 25

A Type-Theoretic Framework for Certified Meta-programming (I...

引用

2025 Workshop on Partial Evaluation and Program Manipulation

作者： Pientka, Brigitte McGill Univ Montreal PQ Canada

ISBN: (纸本)9798400713507

meta-programming is the art of writing programs that produce or manipulate other programs. This allows programmers to automate error-prone or repetitive tasks, and exploit domain-specific knowledge to customize the generated code. Unfortunately, writing safe meta-programs remains very challenging, since errors in the generated code are usually only detected when running it, but not at the time when code is generated. How can we design a flexible and expressive meta-programming framework where we provide a range of safety guarantees about the code that is being generated and the code generator itself? We revisit Cocon, a type-theoretic framework for certified meta-programming. Cocon is two-level type theory: at its base is the logical framework LF where we can represent domain-specific languages (DSL) ranging from simply-typed to polymorphic languages;on top sits a Martin-L of type theory where we can write recursive programs and proofs about those DSLs using pattern matching. In particular, when the DSL is contained in Martin-L of type theory we can use reflection and leverage MLTT's evaluation to execute programs written in a given DSL. Hence, we can derive type-safe meta-programming systems for a range of DSLs.

关键词： Type Theory meta-programming

来源：评论

学校读者我要写书评

暂无评论

Layered Modal Type Theory Where meta-programming Meets Intensional Analysis 33rd

Layered Modal Type Theory Where Meta-programming Meets Inten...

引用

33rd European Symposium on programming (ESOP)

作者： Hu, Jason Z. S. Pientka, Brigitte McGill Univ Sch Comp Sci Montreal PQ H3A 0E9 Canada

ISBN: (纸本)9783031572616;9783031572623

We introduce layering to modal type theory to combine type theory with intensional analysis. In particular, we demonstrate this idea by developing a 2-layered modal type theory. At the core of this type theory (layer 0) is a simply typed.-calculus with no modality. Layer 1 is obtained by extending the core language with one layer of contextual. types to support pattern matching on potentially open code from layer 0 while retaining normalization. Although both layers fundamentally share the same language and the same typing judgment, we only allow computation at layer 1. As a consequence, layer 0 accurately captures the syntactic representation of code in contrast to the computational behaviors at layer 1. The system is justified by normalization by evaluation (NbE) using a presheaf model. The normalization algorithm extracted from the model is sound and complete and is implemented in Agda. Layered modal type theory provides a uniform foundation for metaprogramming with intensional analysis. We see this work as an important step towards a foundational way to support meta-programming in proof assistants.

关键词： modal type theory contextual types meta-programming normalization by evaluation presheaf model

来源：评论

学校读者我要写书评

暂无评论

meta-programming Design-Flow Patterns for Automating Reusable Optimisations 2022

Meta-Programming Design-Flow Patterns for Automating Reusabl...

引用

12th International Symposium on Highly Efficient Accelerators and Reconfigurable Technologies (HEART)

作者： Vandebon, Jessica Coutinho, Jose G. F. Luk, Wayne Imperial Coll London London England

ISBN: (纸本)9781450396608

Continuing advances in heterogeneous and parallel computing enable massive performance gains in domains such as AI and HPC. Such gains often involve using hardware accelerators, such as FPGAs and GPUs, to speed up specific workloads. However, to make effective use of emerging heterogeneous architectures, optimisation is typically done manually by highly-skilled developers with in-depth understanding of the target hardware. The process is tedious, error-prone, and must be repeated for each new application. This paper introduces Design-Flow Patterns, which capture modular, recurring application-agnostic elements involved in mapping and optimising application descriptions onto efficient CPU and GPU targets. Our approach is the first to codify and programmatically coordinate these elements into fully automated, customisable, and reusable end-to-end design-flows. We implement key design-flow patterns using the meta-programming tool Artisan, and evaluate automated design-flows applied to three sequential C++ applications. Compared to single-threaded implementations, our approach generates multi-threaded OpenMP CPU designs achieving up to 18 times speedup on a CPU platform with 32-threads, as well as HIP GPU designs achieving up to 1184 times speedup on an NVIDIA GeForce RTX 2080 Ti GPU.

关键词： Heterogeneous Computing Parallel Computing meta-programming GPU Multi-Core Patterns

来源：评论

学校读者我要写书评

暂无评论

Enhancing High-Level Synthesis Using a meta-programming Approach

引用

IEEE TRANSACTIONS ON COMPUTERS 2021年第12期70卷 2043-2055页

作者： Vandebon, Jessica Coutinho, Jose G. F. Luk, Wayne Nurvitadhi, Eriko Imperial Coll London London SW7 2BX England Intel Corp San Jose CA 95134 USA

In today's increasingly heterogeneous compute landscape, there is high demand for design tools that offer seemingly contradictory features: portable programming abstractions that hide underlying architectural detail, and the capability to optimise and exploit architectural features. Our meta-programming approach, Artisan, decouples application functionality from optimisation concerns to address the complexity of mapping high-level application descriptions onto heterogeneous platforms from which they are abstracted. With Artisan, application experts focus on algorithmic behaviour, while platform and domain experts focus on optimisation and mapping. Artisan offers complete design-flow orchestration in a unified programming environment based on Python 3 to enable accessible codification of reusable optimisation strategies that can be automatically applied to high-level application descriptions. We have developed and evaluated an Artisan prototype and a set of customised meta-programs used to automatically optimise six case study applications for CPU+FPGA targets. In our experiments, Artisan-optimised designs achieve the same order of magnitude speedup as manually optimised designs compared to corresponding unoptimised software.

关键词： Optimization Tools Kernel Software Task analysis Python programming Heterogeneous computing meta-programming FPGA high-level synthesis

来源：评论

学校读者我要写书评

暂无评论

In Praise of Impredicativity: A Contribution to the Formalization of meta-programming

引用

THEORY AND PRACTICE OF LOGIC programming 2020年第1期20卷 99-146页

作者： Bry, Francois Ludwig Maximilian Univ Munich Inst Informat Munich Germany

Processing programs as data is one of the successes of functional and logic programming. Higher-order functions, as program-processing programs are called in functional programming, and meta-programs, as they are called in logic programming, are widespread declarative programming techniques. In logic programming, there is a gap between the meta-programming practice and its theory: The formalizations of meta-programming do not explicitly address its impredicativity and are not fully adequate. This article aims at overcoming this unsatisfactory situation by discussing the relevance of impredicativity to meta-programming, by revisiting former formalizations of meta-programming, and by defining Reflective Predicate Logic, a conservative extension of first-order logic, which provides a simple formalization of meta-programming.

关键词： logic programming meta-programming model theory Barber Paradox Russell's Paradox reflection

来源：评论

学校读者我要写书评

暂无评论

Accelerating Winograd Convolutions using Symbolic Computation and meta-programming 20

Accelerating Winograd Convolutions using Symbolic Computatio...

引用

15th European Conference on Computer Systems (EuroSys)

作者： Mazaheri, Arya Beringer, Tim Moskewicz, Matthew Wolf, Felix Jannesari, Ali Tech Univ Darmstadt Dept Comp Sci Darmstadt Germany Tesla Inc Palo Alto CA USA Iowa State Univ Dept Comp Sci Ames IA USA

ISBN: (纸本)9781450368827

Convolution operations are essential constituents of convolutional neural networks. Their efficient and performance portable implementation demands tremendous programming effort and fine-tuning. Winograd's minimal filtering algorithm is a well-known method to reduce the computational complexity of convolution operations. Unfortunately, existing implementations of this algorithm are either vendor specific or hard-coded to support a small subset of convolutions, thus limiting their versatility and performance portability. In this paper, we propose a novel method to optimize Winograd convolutions based on symbolic computation. Taking advantage meta-programming and auto-tuning, we further introduce a system to automate the generation of efficient and portable Winograd convolution code for various GPUs. We show that our optimization technique can effectively exploit repetitive patterns, enabling us to reduce the number of arithmetic operations by up to 62% without compromising numerical stability. Moreover, we demonstrate in experiments that we can generate efficient kernels with runtimes close to deep-learning libraries, requiring only a minimum of programming effort, which confirms the performance portability of our approach.

关键词： Deep learning Winograd convolution meta-programming symbolic computation

来源：评论

学校读者我要写书评

暂无评论

meta-programming for Cross-Domain Tensor Optimizations 2018

Meta-programming for Cross-Domain Tensor Optimizations

引用

17th ACM SIGPLAN International Conference on Generative programming - Concepts and Experiences (GPCE) part of the SPLASH Collection of Conferences and Workshops

作者： Susungi, Adilla Rink, Norman A. Cohen, Albert Castrillon, Jeronimo Tadonki, Claude PSL Res Univ MINES ParisTech Paris France Tech Univ Dresden Chair Compiler Construct Dresden Germany INRIA Villers Les Nancy France ENS DI Paris France

ISBN: (纸本)9781450360456

Many modern application domains crucially rely on tensor operations. The optimization of programs that operate on tensors poses difficulties that are not adequately addressed by existing languages and tools. Frameworks such as TensorFlow offer good abstractions for tensor operations, but target a specific domain, i.e. machine learning, and their optimization strategies cannot easily be adjusted to other domains. General-purpose optimization tools such as Pluto and existing meta-languages offer more flexibility in applying optimizations but lack abstractions for tensors. This work closes the gap between domain-specific tensor languages and general-purpose optimization tools by proposing the Tensor optimizations meta-Language (TEML). Ton offers high-level abstractions for both tensor operations and loop transformations, and enables flexible composition of transformations into effective optimization paths. This compositionality is built into TEML's design, as our formal language specification will reveal. We also show that TEML can express tensor computations as comfortably as TensorFlow and that it can reproduce Pluto's optimization paths. Thus, optimized programs generated by TEML execute at least as fast as the corresponding Pluto programs. In addition, TEML enables optimization paths that often allow outperforming Pluto.

关键词： tensor algebra meta-programming code generation and optimization denotational semantics

来源：评论

学校读者我要写书评

暂无评论

SpringBoard: game-agnostic tool for scenario editing with meta-programming support

引用

APPLIED INTELLIGENCE 2018年第5期48卷 1161-1175页

作者： Petrovic, Gajo Fujita, Hamido Iwate Prefectural Univ Takizawa Japan

Although we have recently seen an increase of good, free game engine editors, general purpose scenario (level) editors are still lagging behind in terms of functionalities and ease of use. Using them to create game scenarios can be difficult as they often expose general engine capabilities instead of limiting the toolset to fit game-specific requirements. They often require programming skills to use, which introduce additional user skill requirements, and configuring them for a specific game can be equally difficult. In this paper we have developed SpringBoard, an open source scenario editor for games using the SpringRTS engine. Extending it to support game and level requirements is achieved with multi-level meta-programming, while still providing a system that is integrated with the GUI editor and therefore intuitive to use. Our meta-programming system has support for trigger elements (events, functions and actions), custom (composite) data types, scoped data access, higher order functions and actions, and data synchronization mechanics. This novel approach allows us to have the full expressiveness of the underlying programming language, while exposing a user-friendly GUI that consists of terminology familiar to the domain expert.

关键词： Scenario editor Level editor Game creation tool meta-programming

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：