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

14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC)

作者： Bogdanas, Denis Alexandru Ioan Cuza Univ Fac Comp Sci Iasi Romania

ISBN: (纸本)9780769549347;9781467350266

A programming language definition consists of two parts: syntax and semantics. K Framework is an actively developed formalism aimed to address the semantics part. While K has its own capabilities to define syntax and to perform parsing, those are often not expressive enough to handle real world programming languages. Therefore K Framework was designed to be connected to an external parser. In this case the semantics is defined over the representation of programs as AST (Abstract Syntax Tree), and is called label-based. This technique was successfully used to define C language. In this paper we present a parser generator which accepts as input a grammar in SDF format, and produces a parser ready to be integrated with K. We illustrate the methodology of defining a language using the generated parser based on an example. The example definition emphasizes distinctive features of the integration of SDF syntax and K semantics. It also illustrates syntax constructs which are difficult to handle with K Framework alone, but are straightforward to express in SDF + K combination.

关键词： C language context-free grammars programming language semantics

来源：评论

学校读者我要写书评

暂无评论

A Theorem Proving Approach to programming language semantics 23

A Theorem Proving Approach to Programming Language Semantics

引用

IEEE/ACM 45th International Conference on Software Engineering - Software Engineering Education and Training (ICSE-SEET)

作者： Roy, Subhajit Indian Inst Technol Kanpur Kanpur India

ISBN: (纸本)9798350322590

The semantics of programming languages is one of the core topics in computer science. This topic is formalism-heavy and requires the student to attempt numerous proofs for a deep understanding. We argue that modern theorem provers are excellent aids to teaching and understanding programming language semantics. As pen-and-paper proofs get automated via the theorem prover, it allows an experiment-driven strategy at exploring this topic. This article provides an encoding of the semantics of the WHILE language in the most popular styles-operational, denotational, and axiomatic-within the F* proof assistant. We show that once the program and its semantics are encoded, modern proof assistants can prove exciting language features with minimal human assistance. We believe that teaching programming languages via proof assistants will not only provide a more concrete understanding of this topic but also prepare future programming language researchers to use theorem provers as fundamental tools in their research and not as an afterthought.

关键词： Computer Science Education Interactive Proof Assistants programming language semantics Theorem Proving

来源：评论

学校读者我要写书评

暂无评论

Syntax and operational semantics of a probabilistic programming language with scopes

引用

JOURNAL OF MATHEMATICAL PSYCHOLOGY 2016年 74卷 46-57页

作者： Bruza, Peter D. QUT Sch Informat Syst GPO Box 2434 Brisbane Qld Australia

Dzhafarov and Kujala (2015) have introduced a contextual probability theory called Contextuality-by-Default (C-b-D) which is based on three principles. The first of these principles states that each random variable should be automatically labelled by all conditions under which it is recorded. The aim of this article is to relate this principle to block structured computer programming languages where variables are declared local to a construct called a "scope". Scopes are syntactic constructs which correspond to the notion of condition used by C-b-D. In this way a variable declared in two scopes can be safely overloaded meaning that they can have the same label but preserve two distinct identities without the need to label each variable in each condition as advocated by C-b-D. By means of examples, the notion of a probabilistic-program, or P-program, is introduced which is based on scopes. The semantics of P-programs will be illustrated using the well known relational database language SQL which provides an efficient and understandable operational semantics. A core issue addressed is how to construct a single probabilistic model from the various interim probability distributions returned by each syntactic scope. For this purpose, a probabilistic variant of the natural join operator of relational algebra is used to "glue" together interim distributions into a single distribution. More generally, this article attempts to connect contextuality with probabilistic programming by means of relational database theory. (C) 2016 Published by Elsevier Inc.

关键词： Probabilistic programming Probabilistic modelling programming language semantics Contextuality Contextuality-by-Default

来源：评论

学校读者我要写书评

暂无评论

Full abstraction for PCF

引用

INFORMATION AND COMPUTATION 2000年第2期163卷 409-470页

作者： Abramsky, S Jagadeesan, R Malacaria, P Univ Oxford Oxford England Loyola Univ Chicago IL 60611 USA Queen Mary Univ London London E1 4NS England

An intensional model for the programming language PCF is described in which the types of PCF are interpreted by games and the terms by certain history-free strategies. This model is shown to capture definability in PCF. More precisely, every compact strategy in the model is definable in a certain simple extension of PCF. We then introduce an intrinsic preorder on strategies and show that it satisfies some striking properties such that the intrinsic preorder on function types coincides with the pointwise preorder. We then obtain an order-extensional fully abstract model of PCF by quotienting the intensional model by the intrinsic preorder. This is the first syntax-independent description of the fully abstract model for PCF. (Hyland and Ong have obtained very similar results by a somewhat different route, independently and at the same time. ) We then consider the effective version of our model and prove a universality theorem: every element of the effective extensional model is definable in PCF. Equivalently, every recursive strategy is definable up to observational equivalence. (C) 2000 Academic Press.

关键词： game semantics full abstraction sequentiality PCF functional computation programming language semantics linear logic

来源：评论

学校读者我要写书评

暂无评论

INCREMENTAL EVALUATION FOR ATTRIBUTE GRAMMARS WITH UNRESTRICTED MOVEMENT BETWEEN TREE MODIFICATIONS

引用

ACTA INFORMATICA 1988年第2期25卷 155-178页

作者： REPS, T 1.Computer Sciences Department University of Wisconsin 1210 W. Dayton St. 53706 Madison WI USA

This paper concerns the design of editors that perform checks on a language's context-dependent constraints. Our particular concern is the design of an efficient, incremental analysis algorithm for systems based on the attribute-grammar model of editing. With previous incremental evaluation algorithms for arbitrary noncircular attribute grammars, the editing model required there to be a restriction on the operation that moves the editing cursor: moving the cursor was limited to just a single step in the tree — either to the parent node or to one of the child nodes of the current cursor location. This paper describes a new updating algorithm that can be used when an arbitrary movement of the cursor in the tree is permitted. After an operation that restructures the tree, the tree's attributes can be updated with a cost of 0 ((1+|AFFECTED|)·√m), where m is the size of the tree and AFFECTED is the subset of the tree's attributes that require new values, when the cost is amortized over a sequence of tree modifications. the editing cursor may be moved from its current location to any other node of the tree in a single, unit-cost operation. CR Categories and Subject Descriptors: D.2.3 [Software Engineering]: Coding — program editors; D.2.6 [Software Engineering]: programming Environments; D.3.1 [programming languages]: Formal Definitions and Theory — semantics, syntax D.3.4 [programming languages]: Processors — translator writing systems and compiler generators F.3.2 [Logics and Meanings of Programs]: semantics of programming languages — denotational semantics.

关键词： Incremental programming language semantics Trees editing Editors nonius Current Position single-step language Surgery attribute grammars

来源：评论

学校读者我要写书评

暂无评论

Supercompilation for Martin-Lof's type theory

引用

programming AND COMPUTER SOFTWARE 2015年第3期41卷 170-182页

作者： Klyuchnikov, I. G. Romanenko, S. A. Russian Acad Sci Keldysh Inst Appl Math Moscow 125047 Russia

This paper describes the design and implementation of a TT Lite certifying supercompiler, which transforms a source program into a pair consisting of a residual program and a proof that the residual program is equivalent to the source one. As far as we can judge from the presently available literature, it is the first time that certifying supercompilation is implemented for a nontrivial higher-order functional language. Proofs generated by the TT Lite supercompiler can be verified by the type checker that does not depend on the supercompiler and is not based on supercompilation. This is especially important when reliability of results obtained by means of supercompilation is of primary concern.

关键词： COMPILERS (Computer programs) programming language semantics SYNTAX in programming languages INTUITIONISTIC mathematics MATHEMATICAL optimization

来源：评论

学校读者我要写书评

暂无评论

The Layer-Oriented Approach to Declarative languages for Biological Modeling

引用

PLOS COMPUTATIONAL BIOLOGY 2012年第5期8卷 e1002521-e1002521页

作者： Raikov, Ivan De Schutter, Erik Okinawa Inst Sci & Technol Onna Son Okinawa Japan Univ Antwerp B-2020 Antwerp Belgium

We present a new approach to modeling languages for computational biology, which we call the layer-oriented approach. The approach stems from the observation that many diverse biological phenomena are described using a small set of mathematical formalisms (e.g. differential equations), while at the same time different domains and subdomains of computational biology require that models are structured according to the accepted terminology and classification of that domain. Our approach uses distinct semantic layers to represent the domain-specific biological concepts and the underlying mathematical formalisms. Additional functionality can be transparently added to the language by adding more layers. This approach is specifically concerned with declarative languages, and throughout the paper we note some of the limitations inherent to declarative approaches. The layer-oriented approach is a way to specify explicitly how high-level biological modeling concepts are mapped to a computational representation, while abstracting away details of particular programming languages and simulation environments. To illustrate this process, we define an example language for describing models of ionic currents, and use a general mathematical notation for semantic transformations to show how to generate model simulation code for various simulation environments. We use the example language to describe a Purkinje neuron model and demonstrate how the layer-oriented approach can be used for solving several practical issues of computational neuroscience model development. We discuss the advantages and limitations of the approach in comparison with other modeling language efforts in the domain of computational biology and outline some principles for extensible, flexible modeling language design. We conclude by describing in detail the semantic transformations defined for our language.

关键词： Ionic current Neurons Computer software Syntax Linguistics programming language semantics Simulation and modeling programming languages

来源：评论

学校读者我要写书评

暂无评论

Confluence in concurrent constraint programming

引用

THEORETICAL COMPUTER SCIENCE 1997年第2期183卷 281-315页

作者： Falaschi, M Gabbrielli, M Marriott, K Palamidessi, C UNIV PISA DIPARTIMENTO INFORMAT PISA ITALY MONASH UNIV DEPT COMP SCI CLAYTON VIC 3168 AUSTRALIA DEPT COMP SCI & ENGN UNIVERSITY PK PA 16802 USA

Concurrent constraint programming (ccp), like most of the concurrent paradigms, has a mechanism of global choice which makes computations dependent on the scheduling of processes. This is one of the main reasons why the formal semantics of ccp is more complicated than the one of its deterministic and local-choice sublanguages. In this paper we study various subsets of ccp obtained by adding some restriction on the notion of choice, or by requiring confluency, i.e. independency from the scheduling strategy. We show that it is possible to define simple denotational semantics for these subsets, for various notions of observables, Finally, as an application of our results we develop a framework for the compositional analysis of full ccp. The basic idea is to approximate an arbitrary ccp program by a program in the restricted language, and then analyze the latter, by applying the standard techniques of abstract interpretation to its denotational semantics.

关键词： Subset programming language semantics sublanguages indium scheduling policy deterministic programming analysis programme constraint handling

来源：评论

学校读者我要写书评

暂无评论

Modelling contextuality by probabilistic programs with hypergraph semantics

引用

THEORETICAL COMPUTER SCIENCE 2018年 752卷 56-70页

作者： Bruza, Peter D. Queensland Univ Technol Sch Informat Syst GPO Box 2434 Brisbane Qld 4001 Australia

Models of a phenomenon are often developed by examining it under different experimental conditions, or measurement contexts. The resultant probabilistic models assume that the underlying random variables, which define a measurable set of outcomes, can be defined independent of the measurement context. The phenomenon is deemed contextual when this assumption fails. Contextuality is an important issue in quantum physics. However, there has been growing speculation that it manifests outside the quantum realm with human cognition being a particularly prominent area of investigation. This article contributes the foundations of a probabilistic programming language that allows convenient exploration of contextuality in wide range of applications relevant to cognitive science and artificial intelligence. Using the style of syntax employed by the probabilistic programming language WebPPL, specific syntax is proposed to allow the specification of "measurement contexts". Each such context delivers a partial model of the phenomenon based on the associated experimental condition described by the measurement context. An important construct in the syntax determines if and how these partial models can be consistently combined into a single model of the phenomenon. The associated semantics are based on hypergraphs in two ways. Firstly, if the schema of random variables of the partial models is acyclic, a hypergraph approach from relational database theory is used to compute a join tree from which the partial models can be combined to form a single joint probability distribution. Secondly, if the schema is cyclic, measurement contexts are mapped to a hypergraph where edges correspond to sets of events denoting outcomes in measurement contexts. Recent theoretical results from the field of quantum physics show that contextuality can be equated with the possibility of constructing a probabilistic model on the resulting hypergraph. The use of hypergraphs opens the door for a theoreticall

关键词： Probabilistic programming Probabilistic modelling programming language semantics Contextuality

来源：评论

学校读者我要写书评

暂无评论

Scenario-Based Algorithmics: Coding Algorithms by Automatic Composition of Separate Concerns

引用

COMPUTER 2021年第10期54卷 95-101页

作者： Harel, David Marron, Assaf Yerushalmi, Raz Weizmann Inst Sci IL-76100 Rehovot Israel

A method for programming reactive systems, called scenario-based algorithmics, can have several advantages, both in programming and in computer science education. We provide new examples, experiments, and perspectives.

关键词： Formal Specification Functional programming programming language semantics Automatic Composition Separate Concerns programming Reactive Systems Called Scenario Based Algorithmics Computer Science Education Encoding Computer Science Education programming Profession

来源：评论

学校读者我要写书评

暂无评论

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

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：