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

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

作者： Kobayashi, Naoki Tohoku Univ Sendai Miyagi 980 Japan

ISBN: (纸本)9780769544120

The model checking of higher-order recursion schemes (higher-order model checking for short) has been actively studied in the last decade, and has seen significant progress in both theory and practice. From a practical perspective, higher-order model checking provides a foundation for software model checkers for functional programming languages such as ML and Haskell. This short article aims to provide an overview of the recent progress in higher-order model checking and discuss future directions.

关键词： Model checking higher-order theories functional programming language Computer programming languages functional programming

来源：评论

学校读者我要写书评

暂无评论

Introducing Support for Erlang into SSQSA framework

Introducing Support for Erlang into SSQSA framework

引用

International Conference on Numerical Analysis and Applied Mathematics (ICNAAM)

作者： Toth, Melinda Pater-Reszeg, Attila Rakic, Gordana Eotvos Lorand Univ Fac Informat Dept Programming Languages & Compilers H-1364 Budapest Hungary ELTE Soft Ltd Budapest Hungary Univ Novi Sad Fac Sci Dept Math & Informat YU-21000 Novi Sad Serbia

ISBN: (纸本)9780735412873

Set of Software Quality Static Analyzers (SSQSA) is a framework which includes set of software tools for static analysis. Starting aim of the framework is consistent software quality analysis. The main characteristic of all integrated tools is the independency of the input programming language. Each of the integrated analysers can be uniformly applied to any software systems that are written in different programming languages. In SSQSA framework, language independency is achieved by enriched Concrete Syntax Tree (eCST). eCST is used as an internal representation of the source code. Currently, SSQSA supports some representative input languages. Still the support for functional language is missing. For introducing the support for new input language into SSQSA framework straightforward semi-automated procedure is established. In this paper we explore possibility to add support for functional languages into SSQSA framework. Furthermore, we describe alternative way to add support for new language. Described research is made on the case of Erlang.

关键词： enriched concrete syntax tree semantic graph static analysis functional programming language Erlang

来源：评论

学校读者我要写书评

暂无评论

Robin Milner, a Craftsman of Tools for the Mind

Robin Milner, a Craftsman of Tools for the Mind

引用

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

作者： Plotkin, Gordon D. Univ Edinburgh Sch Informat Lab Fdn Comp Sci Edinburgh Midlothian Scotland

The paper discusses about the programming language ML (or Metalanguage) as a language for manipulating formal systems. It has also had much influence on the further development of functional programming languages.

ISBN: (纸本)9780769541143

关键词： ML language formal system manipulation functional programming language meta language programming languages

来源：评论

学校读者我要写书评

暂无评论

Mechanical verification of interactive programs specified by use cases 3

Mechanical verification of interactive programs specified by...

引用

IEEE/ACM 3rd FME Workshop on Formal Methods in Software Engineering

作者： Claret, Guillaume Regis-Gianas, Yann Univ Paris Diderot Sorbonne Paris Cite PPS CNRSUMR 7126PiR2INRIA Paris Rocquencourt F-75205 Paris France

ISBN: (纸本)9781467370431

Interactive programs, like user interfaces, are hard to formally specify and thus to prove correct. Some ideas coming from functional programming languages have been successful to improve the way we write safer programs, compared to traditional imperative languages, but these ideas mostly apply to code fragments without any inputs-outputs. Using the purely functional language Coq, we present a new technique to represent interactive programs and formally verify use cases using the Coq proof engine as a symbolic debugger. To this end we introduce the notion of scenarios, well-typed schema of interactions between an environment and a program. We design and certify a blog system as an illustration. Our approach generalizes unit-testing techniques and outlines a new method for mechanically assisted checking of effectful functional programs.

关键词： mechanical verification Interactive programs functional programming User Interface Device Component ILLUSTRATIONS functional programming language

来源：评论

学校读者我要写书评

暂无评论

ML Polymorphism of Linear Lambda Calculus with First-class Continuations 19

ML Polymorphism of Linear Lambda Calculus with First-class C...

引用

8th International Conference on Software and Computer Applications (ICSCA)

作者： Nishizaki, Shin-ya Tokyo Inst Technol 2-12-1 Ookayama Meguro Tokyo 1528552 Japan

ISBN: (纸本)9781450365734

The Curry-Howard isomorphism shows that an intuitionistic deductive system is similar to a formal computational system;propositions correspond to types, proofs to lambda-terms, and a proof normalization procedure to an evaluation strategy. Furthermore, the duality between computation values and continuations is discovered under the Curry-Howard isomorphism. In the traditional lambda calculus, duplication and erasing of values are allowed but those of continuations prohibited. On the other hand, in the lambda calculus with first-class continuations, both values and continuations are permitted to be duplicated and erased. In our previous paper, we proposed a linear lambda calculus with first-class continuations, in which we cannot duplicate and erase values but can do continuations. In this paper, we propose an ML polymorphic type system for the linear lambda calculus with first-class continuations and design a type inference algorithm of the type system.

关键词： programming language theory functional programming language lambda calculus linear logic continuations Curry-Howard isomorphism ML type system

来源：评论

学校读者我要写书评

暂无评论

The pitfalls of protocol design Attempting to write a formally verified PDF parser

The pitfalls of protocol design Attempting to write a formal...

引用

35th IEEE-Computer-Society Workshop on Security and Privacy (SP)

作者： Bogk, Andreas Schoepl, Marco HERE Berlin Germany Humboldt Univ Inst Informat Berlin Germany

ISBN: (纸本)9781479951031

Parsers for complex data formats generally present a big attack surface for input-driven exploitation. In practice, this has been especially true for implementations of the PDF data format, as witnessed by dozens of known vulnerabilities exploited in many real world attacks, with the Acrobat Reader implementation being the main target. In this report, we describe our attempts to use Coq, a theorem prover based on a functional programming language making use of dependent types and the Curry-Howard isomorphism, to implement a formally verified PDF parser. We ended up implementing a subset of the PDF format and proving termination of the combinator-based parser. Noteworthy results include a dependent type representing a list of strictly monotonically decreasing length of remaining symbols to parse, which allowed us to show termination of parser combinators. Also, difficulties showing termination of parsing some features of the PDF format readily translated into denial of service attacks against existing PDF parsers-we came up with a single PDF file that made all the existing PDF implementations we could test enter an endless loop.

关键词： document handling functional programming grammars security of data theorem proving Acrobat Reader implementation Coq Curry-Howard isomorphism PDF data format combinator-based parser complex data formats denial of service attacks formally verified PDF parser functional programming language input-driven exploitation parser combinators protocol design theorem prover Indexes Portable document format Privacy Security Software Syntactics Writing Portable document format functional programming language PDF gene electronic document handling Parser syntax Data Security theorem proving functional programming DoS attack Writing Privacy Parsing computer software data formats

来源：评论

学校读者我要写书评

暂无评论

The Problem with Data 14

The Problem with Data

引用

IEEE/ACM 7th International Conference on Utility and Cloud Computing (UCC)

作者： Fritsch, Joerg Walker, Coral Cardiff Univ Sch Comp Sci & Informat Cardiff CF24 3AA S Glam Wales

ISBN: (纸本)9781479978816

Utility Computing requires levels of efficacy and abstraction that are not matched by modern computing clouds. In this paper we argue that the lack of harmonization of data and computation is holding back computing clouds from evolving further into utility clouds. Data gravity is perceived as gravity pull associated with data volume. Data of large volume develop large gravity that pulls computation to it, which contrasts with the computation-centered principle of current computing clouds, where computational resources are centralized and fixed. Based on previous research, eight principles are identified to suggest an infrastructure for a future data-driven utility computing platform. The paper also argues that tuple spaces and functional programming languages together would be a powerful combination to meet the requirements for this next-generation computing utility.

关键词： functional languages functional programming utility programs centralized-fixed computational resources computation-centered principle data computation data gravity data harmonization data volume data-driven utility computing platform functional programming languages gravity pull next-generation computing utility tuple spaces Cloud computing Computational modeling Data models Distributed databases Fabrics Gravity programming functional programming Utility routines distributed databases Gravity data models Cloud Computing Computational modeling Textile fabrics fabric programming Utility computing functional programming language Clouds

来源：评论

学校读者我要写书评

暂无评论

REDUCTION BY MESSAGE-PASSING AND ITS IMPLEMENTATION ON TRANSPUTER NETWORK

REDUCTION BY MESSAGE-PASSING AND ITS IMPLEMENTATION ON TRANS...

引用

4TH TRANSPUTER / OCCAM INTERNATIONAL CONF

作者： NUNOKAWA, H NOGUCHI, S

来源：评论

学校读者我要写书评

暂无评论

Extracting Environments from Function Closures 2022

Extracting Environments from Function Closures

引用

11th International Conference on Software and Computer Applications, ICSCA 2022

作者： Nishizaki, Shin-Ya Takayanagi, Yuta Global Scientific Information and Computing Center Tokyo Institute of Technology Tokyo Japan

ISBN: (纸本)9781450385770

In this paper, we study the mechanism for extracting the environment from a function closure in the framework of the lambda calculus. We propose the lambda calculus with environment extraction, which extends environment calculus. We define the untyped calculus: the syntax and the operational semantics. We show that the operational semantics are consistent using translation of the lambda calculus with environment extraction into the lambda calculus with records and pairs. Next, we give a simple type theory to the lambda calculus with environment extraction and prove that the type system holds the subject reduction theorem. © 2022 ACM.

关键词： environment function closure lambda calculus functional programming language

来源：评论

学校读者我要写书评

暂无评论

An analysis method of topological relations between Snort rules

引用

Journal of Southeast University(English Edition) 2016年第1期32卷 21-28页

作者：殷奕汪芸 Takahashi Naohisa 东南大学计算机科学与工程学院南京211189 南京师范大学计算机科学与技术学院南京210023 Department of Computer Science and Engineering Graduate School of Engineering Nagoya Institute of Technology

It is difficult to knowall the relations between Snort rules. To deal with this problem, the topological relations between Snort rules are classified based on the set theory, and a method for calculating the topological relations between Snort rules is proposed. In the existing methods for analyzing the relations of Snort rules, the relations are usually determined only according to the header information of the Snort rules. Without considering the actions of Snort rules, the proposed method improves upon the existing methods and it can classify and calculate the topological relations between Snort rules according to both headers and options information of Snort rules. In addition, the proposed method is implemented by the functional language Haskell. The experimental results showthat the topological relations between Snort rules can be calculated rapidly and effectively. The proposed method also provides an important basis for conflict detection in the succeeding Snort rules.

关键词： intrusion detection system（IDS） Snort rule functional programming language

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：