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

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

来源：评论

学校读者我要写书评

暂无评论

meta-programming With Built-in Type Equality

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2008年 199卷 49-65页

作者： Sheard, Tim Pasalic, Emir Portland State Univ Dept Comp Sci Portland OR 97207 USA Rice Univ Dept Comp Sci Houston TX 77251 USA

We report our experience with exploring a new point in the design space for formal reasoning systems: the development of the programming language Omega mega. Omega mega is intended as both a practical programming language and a logic. The main goal of Omega mega is to allow programmers to describe and reason about semantic properties of programs from within the programming language itself, mainly by using a powerful type system. We illustrate the main features of Omega mega by developing an interesting meta-programming example. First, we show how to encode a set of well-typed simply typed lambda- calculus terms as an Omega mega data-type. Then, we show how to implement a substitution operation on these terms that is guaranteed by the Omega mega type system to preserve their well-typedness.

关键词： meta-programming meta-language Equality types

来源：评论

学校读者我要写书评

暂无评论

meta-programming Event-B Advancing Tool Support and Language Extensions 10th

Meta-programming Event-B Advancing Tool Support and Language...

引用

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

来源：评论

学校读者我要写书评

暂无评论

meta-programming and Auto-tuning in the Search for High Performance GPU Code 4

Meta-programming and Auto-tuning in the Search for High Perf...

引用

4th ACM SIGPLAN Workshop on Functional High-Performance Computing (FHPC)

作者： Vollmer, Michael Svensson, Bo Joel Holk, Eric Newton, Ryan R. Indiana Univ Bloomington IN 47405 USA

ISBN: (纸本)9781450338073

Writing high performance GPGPU code is often difficult and time-consuming, potentially requiring laborious manual tuning of low-level details. Despite these challenges, the cost in ignoring GPUs in high performance computing is increasingly large. Auto-tuning is a potential solution to the problem of tedious manual tuning. We present a framework for auto-tuning GPU kernels which are expressed in an embedded DSL, and which expose compile-time parameters for tuning. Our framework allows for kernels to be polymorphic over what search strategy will tune them, and allows search strategies to be implemented in the same metalanguage as the kernel-generation code (Haskell). Further, we show how to use functional programming abstractions to enforce regular (hyper-rectangular) search spaces. We also evaluate several common search strategies on a variety of kernels, and demonstrate that the framework can tune both EDSL and ordinary CUDA code.

关键词： auto-tuning meta-programming parallelism GPUs

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

Improving the lower bounds on inequivalent Hadamard matrices through orthogonal designs and meta-programming techniques

引用

APPLIED NUMERICAL MATHEMATICS 2010年第4期60卷 370-377页

作者： Koukouvinos, Christos Simos, Dimitris E. Natl Tech Univ Athens Dept Math GR-15773 Athens Greece

In this paper, we construct inequivalent Hadamard matrices based on several new and old full orthogonal designs, using circulant and symmetric block matrices. Not all orthogonal designs produce inequivalent Hadamard matrices, because the corresponding systems of equations do not possess solutions. In addition, we give some new constructions for orthogonal designs derived from sequences with zero autocorrelation. The orthogonal designs used to construct the inequivalent Hadamard matrices are produced from theoretical and algorithmic constructions. (C) 2009 IMACS. Published by Elsevier By. All rights reserved.

关键词： Hadamard matrices Orthogonal designs Sequences Non-periodic autocorrelation function meta-programming

来源：评论

学校读者我要写书评

暂无评论

PROGRAM LOGICS FOR HOMOGENEOUS GENERATIVE RUN-TIME meta-programming

引用

LOGICAL METHODS IN COMPUTER SCIENCE 2015年第1期11卷

作者： Berger, Martin Tratt, Laurence Univ Sussex Dept Informat Brighton BN1 9QJ E Sussex England Kings Coll London Dept Informat Software Dev Team London WC2R 2LS England

This paper provides the first program logic for homogeneous generative run-time meta-programming using a variant of MiniML(e)(square) by Davies and Pfenning as its underlying on language. We show the applicability of our approach by reasoning about example meta-programs from the literature. We also demonstrate that our logics are relatively complete in the sense of Cook, enable the inductive derivation of characteristic formulae, and exactly capture the observational properties induced by the operational semantics.

关键词： Program Logic Specification Verification meta-programming Types Observational Completeness Descriptive Completeness Relative Completeness Characteristic Formula

来源：评论

学校读者我要写书评

暂无评论

meta-programming through typeful code representation 03

Meta-programming through typeful code representation

引用

8th International Conference on Functional programming (ICFP 03)

作者： Chen, CY Xi, HW Boston Univ Comp Sci Dept Boston MA 02215 USA

ISBN: (纸本)9781581137569

By allowing the programmer to write code that can generate code at run-time, meta-programming offers a powerful approach to program construction. For instance, meta-programming can often be employed to enhance program efficiency and facilitate the construction of generic programs. However, meta-programming, especially in an untyped setting, is notoriously error-prone. In this paper, we aim at making meta-programming less error-prone by providing a type system to facilitate the construction of correct meta-programs. We first introduce some code constructors for constructing typeful code representation in which program variables are replaced with deBruijn indices, and then formally demonstrate how such typeful code representation can be used to support meta-programming. The main contribution of the paper lies in recognition and then formalization of a novel approach to typed meta-programming that is practical, general and flexible.

关键词： meta-programming multi-level staged programming typeful code representation

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：