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

15th International Workshop on Logical and Semantic Frameworks, with Applications (LSFA)

作者： Manzino, Cecilia Pardo, Alberto Univ Nacl Rosario Dept Ciencias Comp Rosario Santa Fe Argentina Univ Republica Inst Comp Montevideo Uruguay

The analysis of information flow is a popular technique for ensuring the confidentiality of data. It is in this context that confidentiality policies arise for giving guarantees that private data cannot be inferred by the inspection of public data. One of those policies is non-interference, a semantic condition that ensures the absence of illicit information flow during program execution by not allowing to distinguish the results of two computations when they only vary in their confidential inputs. A remarkable feature of non-interference is that it can be enforced statically by the definition of information flow type systems. In those type systems, if a program type-checks, then it means that it meets the security policy. In this paper we focus on the preservation of non-interference through program translation. Concretely, we formalize the proof of security preservation of Hunt and Sands' translation that transforms high-level While programs typable in a flow-sensitive type system into equivalent high-level programs typable in a flow-insensitive type system. Our formalization is performed in the dependently-typed language Agda. We use the expressive power of Agda's type system to encode the security type systems at the type level. A particular aspect of our formalization is that it follows a fully internalist approach where we decorate the type of the abstract syntax with security type information in order to obtain the representation of well-typed (i.e secure) programs. A benefit of this approach is that it allows us to directly express the property of security preservation in the type of the translation relation. In this manner, apart from inherently expressing the transformation of programs, the translation relation also stands for an inductive proof of security preservation.

关键词： non-interference information flow type systems dependently-typed programming Agda type safety

来源：评论

学校读者我要写书评

暂无评论

Agda Formalization of a Security-preserving Translation from Flow-sensitive to Flow-insensitive Security Types

引用

Electronic Notes in Theoretical Computer Science 2020年 351卷 75-94页

作者： Cecilia Manzino Alberto Pardo Departamento de Ciencias de la Computación Universidad Nacional de Rosario Argentina Instituto de Computación Universidad de la RepúblicaMontevideo Uruguay

关键词： non-interference information flow type systems dependently-typed programming Agda type safety

来源：评论

学校读者我要写书评

暂无评论

How to do Proofs Practically Proving Properties about Effectful Programs' Results (Functional Pearl) 4

How to do Proofs Practically Proving Properties about Effect...

引用

4th ACM SIGPLAN International Workshop on Type-Driven Development (TyDe)

作者： Jacobs, Koen Nuyts, Andreas Devriese, Dominique Katholieke Univ Leuven Leuven Belgium Vrije Univ Brussel Brussels Belgium

ISBN: (纸本)9781450368155

dependently-typed languages are great for stating and proving properties of pure functions. We can reason about them modularly (state and prove their properties independently of other functions) and non-intrusively (without modifying their implementation). But what if we are interested in properties about the results of effectful computations? Ideally, we could keep on stating and proving them just as nicely. This pearl shows we can. We formalise a way to lift a property about values to a property about effectful computations producing such values, and we demonstrate that we need not make any sacrifices when reasoning about them. In addition to this modular and non-intrusive reasoning, our approach offers independence of the underlying monad and allows for readable proofs whose structure follows that of the code.

关键词： Agda dependently-typed programming effectful extrinsic proofs monad functor applicative strong specification equational reasoning

来源：评论

学校读者我要写书评

暂无评论

A Type Theoretic Specification of Partial Evaluation 14

A Type Theoretic Specification of Partial Evaluation

引用

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

作者： Asai, Kenichi Fennell, Luminous Thiemann, Peter Zhang, Yang Ochanomizu Univ Tokyo Japan Univ Freiburg Freiburg Germany

ISBN: (纸本)9781450329477

We develop a type theoretic specification of offline partial evaluation for the simply-typed lambda calculus in the dependently-typed programming language Agda. We establish the correctness of the specification by proving termination, typing preservation, and semantics preservation using logical relations. Typing preservation is achieved by relying on a typed syntax representation based on De Bruijn indices for the source and the target language. The full calculus contains primitive recursion on natural numbers and higherorder lifting for function, product, and sum types.

关键词： partial evaluation dependently-typed programming typed metaprogramming

来源：评论

学校读者我要写书评

暂无评论

On the semantics of exceptions for high level and low level languages

On the semantics of exceptions for high level and low level ...

引用

作者： Tejiščák, Matúš Charles University of Prague

The thesis deals with correctness of a compiler of a simple language featuring exceptions. We present formal semantics, both denotational semantics of a~high-level language and operational semantics of a low-level language for a~simple stack machine. We study the method of stack unwinding and then iteratively, improving upon a naive solution, we present a different method that is structurally recursive and thus suitable for implementation in total dependently typed languages. Finally, we provide an implementation of the compiler in the dependently typed functional programming language Agda, along with a mechanically verifiable proof of adherence of the implementation to the semantics.

关键词： dependently-typed programming exceptions certified compiler correctness

来源：评论

学校读者我要写书评

暂无评论

Embedding Polymorphic Dynamic Typing

Embedding Polymorphic Dynamic Typing

引用

7th ACM SIGPLAN Workshop on Generic programming (WGP 2011)

作者： van Noort, Thomas Swierstra, Wouter Achten, Peter Plasmeijer, Rinus Radboud Univ Nijmegen Inst Comp & Informat Sci NL-6500 GL Nijmegen Netherlands

ISBN: (纸本)9781450308618

Dynamic typing in a statically typed functional language allows us to defer type unification until run time. This is typically useful when interacting with the 'outside' world where the type of values involved may not be known statically. Haskell has minimal support for dynamic typing, it only supports monomorphism. Clean, on the other hand, has a more rich and mature dynamic typing system where polymorphism is supported as well. An interesting difference is that Haskell offers monomorphic dynamic typing via a library, while Clean offers polymorphic dynamic typing via built-in language support. In the Clean approach there is a great deal of freedom in the implementation in the compiler since the dynamic typing system is defined on abstract syntax trees, whereas the Haskell approach does not need to extend the core language and hence reduces the complexity of the language and compiler. In this paper we investigate what it takes for a functional language to embed polymorphic dynamic typing. We explore an embedding in Haskell using generalised algebraic datatypes and argue that a universe. for the representation of types needs to separated from its interpretation as a type. We motivate the need for a dependently-typed functional language like Agda and perform the embedding using structural equality on type representations. Finally, we extend this approach with an instance-of algorithm and define a framework for the corresponding cast function.

关键词： dependently-typed programming dynamic typing generalised algebraic datatypes instantiation polymorphism unification universe construction

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：