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

relational parametricity FOR COMPUTATIONAL EFFECTS

LOGICAL METHODS IN COMPUTER SCIENCE 2009年第3期5卷

作者： Mogelberg, Rasmus Ejlers Simpson, Alex IT Univ Copenhagen Copenhagen Denmark Univ Edinburgh Sch Informat LFCS Edinburgh EH8 9YL Midlothian Scotland

According to Strachey, a polymorphic program is parametric if it applies a uniform algorithm independently of the type instantiations at which it is applied. The notion of relational parametricity, introduced by Reynolds, is one possible mathematical formulation of this idea. relational parametricity provides a powerful tool for establishing data abstraction properties, proving equivalences of datatypes, and establishing equalities of programs. Such properties have been well studied in a pure functional setting. Many programs, however, exhibit computational effects, and are not accounted for by the standard theory of relational parametricity. In this paper, we develop a foundational framework for extending the notion of relational parametricity to programming languages with effects.

关键词： relational parametricity computational effects monads intuitionistic set theory

来源：评论

学校读者我要写书评

暂无评论

When does 0-1 Principle Hold for Prefix Sums?

引用

NEW GENERATION COMPUTING 2023年第3期41卷 523-531页

作者： Morihata, Akimasa Univ Tokyo Grad Sch Arts & Sci Komaba 3-8-1 Tokyo 1538902 Japan

Knuth's 0-1 principle argues that the correctness of any swap-based sorting network can be verified by testing arbitrary sequences over Boolean values (i.e., 0 and 1). Voigtlander (Proceedings of the 35th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008. ACM, New York, NY, pp 29-35, 2008. https://***/10.1145/1328438.1328445) proved a similar result for prefix-sum networks that consist of associative binary operators: the correctness can be verified by testing arbitrary sequences and associative binary operators over three values, namely 0, 1, and 2. He raised the question of whether testing over Boolean values is sufficient if the binary operator is idempotent in addition to associative. This paper answers his question. First, there is an incorrect prefix-sum network for associative idempotent operators, the flaw of which cannot be detected by testing over Boolean values. Second, testing over Boolean values is sufficient if the binary operators are restricted to commutative in addition to associative and idempotent.

关键词： Prefix sum 0-1 principle relational parametricity Testing

来源：评论

学校读者我要写书评

暂无评论

Universal properties for universal types in bifibrational parametricity

引用

MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE 2019年第6期29卷 810-827页

作者： Ghani, Neil Forsberg, Fredrik Nordvall Orsanigo, Federico Univ Strathclyde Dept Comp & Informat Sci Glasgow Lanark Scotland

In the 1980s, John Reynolds postulated that a parametrically polymorphic function is an ad-hoc polymorphic function satisfying a uniformity principle. This allowed him to prove that his set-theoretic semantics has a relational lifting which satisfies the Identity Extension Lemma and the Abstraction Theorem. However, his definition (and subsequent variants) has only been given for specific models. In contrast, we give a model-independent axiomatic treatment by characterising Reynolds' definition via a universal property, and show that the above results follow from this universal property in the axiomatic setting.

关键词： relational parametricity categorical semantics comprehension categories

来源：评论

学校读者我要写书评

暂无评论

Ownership confinement ensures representation independence for object-oriented programs

引用

JOURNAL OF THE ACM 2005年第6期52卷 894-960页

作者： Banerjee, A Naumann, DA Kansas State Univ Dept Comp & Informat Sci Manhattan KS 66506 USA Stevens Inst Technol Dept Comp Sci Hoboken NJ 07030 USA

Representation independence formally characterizes the encapsulation provided by language constructs for data abstraction and justifies reasoning by simulation. Representation independence has been shown for a variety of languages and constructs but not for shared references to mutable state;indeed it fails in general for such languages. This article formulates representation independence for classes, in an imperative, object-oriented language with pointers, subclassing and dynamic dispatch, class oriented visibility control, recursive types and methods, and a simple form of module. An instance of a class is considered to implement an abstraction using private fields and so-called representation objects. Encapsulation of representation objects is expressed by a restriction, called confinement, on aliasing. Representation independence is proved for programs satisfying the confinement condition. A static analysis is given for confinement that accepts common designs such as the observer and factory patterns. The formalization takes into account not only the usual interface between a client and a class that provides an abstraction but also the interface (often called "protected") between the class and its subclasses.

关键词： languages verification alias control confinement relational parametricity simulation data refinement

来源：评论

学校读者我要写书评

暂无评论

Logical Relations and parametricity - A Reynolds Programme for Category Theory and Programming Languages

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2014年 303卷 149-180页

作者： Hermida, Claudio Reddy, Uday S. Robinson, Edmund P. Univ Birmingham Birmingham W Midlands England Queen Mary Univ London London England

In his seminal paper on "Types, Abstraction and Parametric Polymorphism," John Reynolds called for homomorphisms to be generalized from functions to relations. He reasoned that such a generalization would allow type-based "abstraction" (representation independence, information hiding, naturality or parametricity) to be captured in a mathematical theory, while accounting for higher-order types. However, after 30 years of research, we do not yet know fully how to do such a generalization. In this article, we explain the problems in doing so, summarize the work carried out so far, and call for a renewed attempt at addressing the problem.

关键词： Universal algebra Category Theory Homomorphisms Logical Relations Natural Transformations Parametric polymorphism relational parametricity Data abstraction Information hiding Definability Reflexive Graphs Fibrations Relation lifting

来源：评论

学校读者我要写书评

暂无评论

Correctness of data representations involving heap data structures

引用

SCIENCE OF COMPUTER PROGRAMMING 2004年第1-3期50卷 129-160页

作者： Reddy, US Yang, H Univ Birmingham Sch Comp Sci Birmingham B15 2TT W Midlands England Korea Adv Inst Sci & Technol Micros Res Ctr Taejon 305701 South Korea

While the semantics of local variables in programming languages is by now well-understood, the semantics of pointer-addressed heap variables is still an outstanding issue. In particular, the commonly. assumed relational reasoning principles or data representations have not been validated in a semantic model of heap variables. In this paper, we define a parametricity semantics for a Pascal-like language with pointers and heap variables which gives such reasoning principles. It turns out that the correspondences between data representations cannot simply be relations between states, but more intricate correspondences that also need to keep track of visible locations whose pointers can be stored and leaked. (C) 2004 Elsevier B.V. All rights reserved.

关键词： denotational semantics relational parametricity separation logic imperative programming languages

来源：评论

学校读者我要写书评

暂无评论

A Generic Operational Metatheory for Algebraic Effects

A Generic Operational Metatheory for Algebraic Effects

引用

25th Annual IEEE Symposium on Logic in Computer Science (LICS)

作者： Johann, Patricia Simpson, Alex Voigtlaender, Janis Univ Strathclyde Glasgow G1 1XH Lanark Scotland Univ Edinburgh Sch Informat Edinburgh Midlothian Scotland Univ Bonn Inst Comp Sci D-53012 Bonn Germany

ISBN: (纸本)9780769541143

We provide a syntactic analysis of contextual preorder and equivalence for a polymorphic programming language with effects. Our approach applies uniformly across a range of algebraic effects, and incorporates, as instances: errors, input/output, global state, nondeterminism, probabilistic choice, and combinations thereof. Our approach is to extend Plotkin and Power's structural operational semantics for algebraic effects (FoSSaCS 2001) with a primitive "basic preorder" on ground type computation trees. The basic preorder is used to derive notions of contextual preorder and equivalence on program terms. Under mild assumptions on this relation, we prove fundamental properties of contextual preorder (hence equivalence) including extensionality properties and a characterisation via applicative contexts, and we provide machinery for reasoning about polymorphism using relational parametricity.

关键词： algebra algebraic effects contextual preorder generic operational metatheory polymorphic programming language programming language semantics relational parametricity structural operational semantics syntactic analysis

来源：评论

学校读者我要写书评

暂无评论

Free Theorems Involving Type Constructor Classes Functional Pearl

Free Theorems Involving Type Constructor Classes Functional ...

引用

14th ACM SIGPLAN International Conference on Functional Programming

作者： Voigtlaender, Janis Tech Univ Dresden Inst Theoret Informat D-01062 Dresden Germany

ISBN: (纸本)9781605583327

Free theorems are a charm, allowing the derivation of useful statements about programs from their (polymorphic) types alone. We show how to reap such theorems not only from polymorphism over ordinary types, but also from polymorphism over type constructors restricted by class constraints. Our prime application area is that of monads, which form the probably most popular type constructor class of Haskell. To demonstrate the broader scope, we also deal with a transparent way of introducing difference lists into a program, endowed with a neat and general correctness proof.

关键词： relational parametricity

来源：评论

学校读者我要写书评

暂无评论

Parametric limits

Parametric limits

引用

19th Annual IEEE Symposium on Logic in Computer Science

作者： Dunphy, B Reddy, US Univ Illinois Chicago IL 60680 USA

ISBN: (纸本)0769521924

We develop a categorical model of polymorphic lambda calculi using the notion of parametric limits, which extend the notion of limits in categories to reflexive graphs of categories. We show that a number of parametric models of polymorphism can be captured in this way. We also axiomatize the structure of reflexive graphs needed for modelling parametric polymorphism based on ideas of fibrations, and show that it leads to proofs of representation results such as the initial algebra and final coalgebra properties one expects in polymorphic lambda calculi.

关键词： parametric polymorphism relational parametricity categorical models fibrations

来源：评论

学校读者我要写书评

暂无评论

Transport via Partial Galois Connections and Equivalences 21st

Transport via Partial Galois Connections and Equivalences

引用

21st Asian Symposium on Programming Languages and Systems (APLAS)

作者： Kappelmann, Kevin Tech Univ Munich Boltzmannstr 3 D-85748 Garching Germany

ISBN: (纸本)9789819983100;9789819983117

Multiple types can represent the same concept. For example, lists and trees can both represent sets. Unfortunately, this easily leads to incomplete libraries: some set-operations may only be available on lists, others only on trees. Similarly, subtypes and quotients are commonly used to construct new type abstractions in formal verification. In such cases, one often wishes to reuse operations on the representation type for the new type abstraction, but to no avail: the types are not the same. To address these problems, we present a new framework that transports programs via equivalences. Existing transport frameworks are either designed for dependently typed, constructive proof assistants, use univalence, or are restricted to partial quotient types. Our framework (1) is designed for simple type theory, (2) generalises previous approaches working on partial quotient types, and (3) is based on standard mathematical concepts, particularly Galois connections and equivalences. We introduce the notions of partial Galois connection and equivalence and prove their closure properties under (dependent) function relators, (co)datatypes, and compositions. We formalised the framework in Isabelle/HOL and provide a prototype.

关键词： Galois connections Equivalences relational parametricity

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：