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

An implementation of syntax directed functional programming on nested-stack machines

Formal Aspects of Computing 1992年第4期4卷 341-375页

作者： Fassbender, Heinz Vogler, Heiko Lehrstuhl für Informatik II RWTH Aachen Aachen Germany

This paper contributes to the field of functional programming languages. We investigate the call-by-name and call-by-need implementation of a restricted type of functional programming, called syntax directed functional programming;the target of this implementation is an abstract machine that is based on nested stacks. In fact, the technical kernel of this paper is a refinement of an automata theoretical result that, roughly speaking, investigates the well-known relationship "recursion = iteration + stack" in the framework of tree transducers. More precisely, in the underlying result the class of functions computed by total deterministic macro tree-to-string transducers with the call-by-name computation strategy is characterized by total deterministic checking-tree nested-stack transducers. Note that total deterministic macro tree-to-string transducers are term rewriting systems by means of which the reduction semantics of syntax directed functional programming languages can be described. © 1992 BCS.

关键词： Formal languages Models of computation semantics of programming languages

来源：评论

学校读者我要写书评

暂无评论

Towards Substructural Property-Based Testing 1

引用

31st International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR)

作者： Mantovani, Marco Momigliano, Alberto Univ Milan Dipartimento Informat Milan Italy

ISBN: (数字)9783030988692

ISBN: (纸本)9783030988692;9783030988685

We propose to extend property-based testing to substructural logics to overcome the current lack of reasoning tools in the field. We take the first step by implementing a property-based testing system for specifications written in the linear logic programming language Lolli. We employ the foundational proof certificates architecture to model various data generation strategies. We validate our approach by encoding a model of a simple imperative programming language and its compilation and by testing its meta-theory via mutation analysis.

关键词： Linear logic Property-based testing Focusing semantics of programming languages

来源：评论

学校读者我要写书评

暂无评论

Formal specification and verification of the C# thread model

Formal specification and verification of the C# thread model

引用

2nd International Symposium on Formal Methods for Components and Objects

作者： Stärk, RF ETH Dept Comp Sci CH-8092 Zurich Switzerland

We present a high-level Abstract State Machine (ASM) model of C# threads and the NET memory model. We focus on purely managed, fully portable threading features of C#. The sequential model interleaves the computation steps of the currently running threads and is suitable for uniprocessors. The parallel model addresses problems of true concurrency on multi-processor systems. The models provide a sound basis for the development of multi-threaded applications in C#. The thread and memory models complete the abstract operational semantics of C# in [Borger et al. Theoret. Comput. Sci., to appear]. The main invariants of the thread model concerning locks, monitors and mutual exclusion are formally verified in the AsmTP system, an interactive proof assistant based on ASM logic. (c) 2005 Elsevier B.V. All rights reserved.

关键词： semantics of programming languages abstract state machines threads memory consistency models C# NET

来源：评论

学校读者我要写书评

暂无评论

Abstraction Analysis and Certified Flow and Context Sensitive Points-to Relation for Distributed Programs

Abstraction Analysis and Certified Flow and Context Sensitiv...

引用

12th International Conference on Computational Science and Its Applications (ICCSA)

作者： El-Zawawy, Mohamed A. Al Imam MISI Univ Coll Comp & Informat Sci Riyadh Saudi Arabia

ISBN: (纸本)9783642311277;9783642311284

This paper presents a new technique for pointer analysis of distributed programs executed on parallel machines with hierarchical memories. One motivation for this research is the languages whose global address space is partitioned. Examples of these languages are Fortress, X10, Titanium, Co-Array Fortran, UPC, and Chapel. These languages allow programmers to adjust threads and data layout and to write to and read from memories of other threads. The techniques presented in this paper have the form of type systems which are simply structured. The proposed technique is shown on a language which is the while langauge enriched with basic commands for pointer manipulations and also enriched with commands vital for distributed execution of programs. An abstraction analysis that for a given statement calculates the set of function abstractions that the statement may evaluate-to is introduced in this paper. The abstraction analysis is needed in the proposed pointer analysis. The mathematical soundness of all techniques presented in this paper are discussed. The soundness is proved against a new operational semantics presented in this paper. Our work has two advantages over related work. In our technique, each analysis result is associated with a correctness proof in the form of type derivation. The hierarchical memory model used in this paper is in line with the hierarchical character of concurrent parallel computers.

关键词： abstraction analysis certified code flow and context sensitive points-to relation distributed programs semantics of programming languages operational semantics

来源：评论

学校读者我要写书评

暂无评论

Step Indexed Realizability semantics for a Call-by-Value Language Based on Basic Combinatorial Objects 12

Step Indexed Realizability Semantics for a Call-by-Value Lan...

引用

27th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

作者： Hoshino, Naohiko Kyoto Univ Math Sci Res Inst Kyoto Japan

ISBN: (纸本)9780769547695

We propose a mathematical framework for step indexed realizability semantics of a call-by-value polymorphic lambda calculus with recursion, existential types and recursive types. Our framework subsumes step indexed realizability semantics by untyped call-by-value lambda calculi as well as categorical abstract machines. Starting from an extension of Hofstra's basic combinatorial objects, we construct a step indexed categorical realizability semantics. Our main result is soundness and adequacy of our step indexed realizability semantics. As an application, we show that a small step operational semantics captures the big step operational semantics of the call-by-value polymorphic lambda calculus. We also give a safe implementation of the call-by-value polymorphic lambda calculus into a categorical abstract machine.

关键词： semantics of programming languages operational semantics denotational semantics

来源：评论

学校读者我要写书评

暂无评论

AXIOMATIZATIONS OF BACKTRACKING 9th

AXIOMATIZATIONS OF BACKTRACKING

引用

9TH ANNUAL SYMP ON THEORETICAL ASPECTS OF COMPUTER SCIENCE ( STACS 92 )

作者： BILLAUD, M LaBRI (Laboratolre Bordelais de Recherche en Inforrnatlque) unité Associée 1304 du C.N.R.S. Université Bordeaux I 351 Cours de la Libération Talence Cedex 33405 France

ISBN: (纸本)3540552103

Goal schemes are terms built from a set of variables (representing goals) and the control structures {false, true, or, and} to which we give a sequential à la Prolog interpretation. We study equivalence relations induced by some interesting classes of elementary goals. We prove that, when goals are allowed to produce side-effects, or when they are restricted to have finite behaviours, there are finite complete axiomatizations that can be used to decide the equivalence of goal schemes. We conjecture that there is no such finite axiomatization in the case of general pure requests. © Springer-Verlag Berlin Heidelberg 1992.

关键词： PROLOG semantics of programming languages FOUNDATIONS OF LOGIC programming DEPTH-1ST SEARCH BACKTRACKING EQUIVALENCE OF PROGRAM SCHEMES ALGEBRAIC semantics

来源：评论

学校读者我要写书评

暂无评论

Expressing Preferences in Logic programming using an Infinite-Valued Logic 15

Expressing Preferences in Logic Programming using an Infinit...

引用

17th International Symposium on Principles and Practice of Declarative programming (PPDP)

作者： Rondogiannis, Panos Troumpoukis, Antonis Univ Athens Dept Informat & Telecommun Athens Greece

ISBN: (纸本)9781450335164

We propose the new logic programming language PrefLog, which is based on an infinite-valued logic in order to support operators for expressing preferences. We demonstrate that if the operators used are continuous over the infinite-valued underlying domain, then the resulting logic programming language retains the well-known properties of classical logic programming (and most notably the existence of a least Herbrand model). We argue that one can define simple and natural new continuous operators by using a small set of operators that are easily shown to be continuous. Finally, we demonstrate that despite the fact that the underlying truth domain and the set of possible interpretations of a PrefLog program are infinite, we can define a terminating bottom-up proof procedure for implementing a significant and useful fragment of the language.

关键词： Logic programming Preferences semantics of programming languages

来源：评论

学校读者我要写书评

暂无评论

Heap Slicing Using Type Systems

Heap Slicing Using Type Systems

引用

12th International Conference on Computational Science and Its Applications (ICCSA)

作者： El-Zawawy, Mohamed A. Al Imam MISI Univ Coll Comp & Informat Sci Riyadh Saudi Arabia

ISBN: (纸本)9783642311369;9783642311376

Using type systems, this paper treats heap slicing which is a technique transforming a program into a new one that produces the same result while working on a heap sliced into independent regions. Heap slicing is a common approach to handle the problem of modifying the heap layout without changing the program semantics. Heap slicing has applications in the areas of performance optimization and security. Towards solving the problem of heap slicing, this paper introduces three type systems. The first type system does a pointer analysis and annotates program points with pointer information. This type system is an augmentation of a previously developed type system by the author. The second type system does a region analysis and refines the result of the first type system by augmenting the pointer information with region information. The region information approximately specifies at each program point for each memory cell the region where the cell exists. The third type system uses the information gathered by the region type system to do the principal transformation of heap slicing. The paper also presents two operational semantics;one for single-region heap scenario and the other for multi-regions heap scenario. These semantics are used to prove the soundness of the type systems.

关键词： heap slicing type systems semantics of programming languages operational semantics region analysis pointer analysis

来源：评论

学校读者我要写书评

暂无评论

Boosting the Software Quality of Parallel programming Using Logical Means 15th

Boosting the Software Quality of Parallel Programming Using ...

引用

15th International Conference on Computational Science and Its Applications (ICCSA)

作者： El-Zawawy, Mohamed A. Al Imam Mohammad Ibn Saud Islamic Univ IMSIU Coll Comp & Informat Sci Riyadh Saudi Arabia Cairo Univ Fac Sci Dept Math Giza 12613 Egypt

ISBN: (纸本)9783319214139;9783319214122

Parallel programming can be realized as a main tool to improve performance. A main model for programming parallel machines is the single instruction multiple data (SIMD) model of parallelism. This paper presents an axiomatic semantics for SIMD programs. This semantics is useful for designating and attesting partial correctness properties for SIMD programs and is a generalization of the separation's logical system (designed for sequential programs). The second contribution of this paper is an operational framework to conventionally define the semantics of SIMD programs. This framework has two sets of inference rules;for running a program on a single machine and for running a program on many machines concurrently. A detailed correctness proof for the presented logical system is presented using the proposed operational semantics. Also the paper presents a detailed example of a specification derivation in the proposed logical system.

关键词： Concurrent separation logic (CSL) Program logic Program verification Concurrency Soundness Distributed programs semantics of programming languages Operational semantics

来源：评论

学校读者我要写书评

暂无评论

The Geometry of Computation-Graph Abstraction 18

The Geometry of Computation-Graph Abstraction

引用

33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) held as part of the Federated Logic Conference (FLoC)

作者： Muroya, Koko Cheung, Steven W. T. Ghica, Dan R. Univ Birmingham Birmingham W Midlands England

ISBN: (纸本)9781450355834

The popular library TENSORFLOW (TF) has familiarised the mainstream of machine-learning community with programming language concepts such as data-flow computing and automatic differentiation. Additionally, it has introduced some genuinely new syntactic and semantic programming concepts. In this paper we study one such new concept, the ability to extract and manipulate the state of a computation graph. This feature allows the convenient specification of parameterised models by freeing the programmer of the bureaucracy of parameter management, while still permitting the use of generic, model-independent, search and optimisation algorithms. We study this new language feature, which we call 'graph abstraction' in the context of the call-by-value lambda calculus, using the recently developed Dynamic Geometry of Interaction formalism. We give a simple type system guaranteeing the safety of graph abstraction, and we also show the safety of critical language properties such as garbage collection and the beta law. The semantic model suggests that the feature could be implemented in a general-purpose functional language reasonably effciently.

关键词： Geometry of Interaction semantics of programming languages TensorFlow

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：