The Java JDK security model provides an access control mechanism for the JVM based on dynamic stack inspection. Previous results have shown how stack inspection can be enforced at compile time via whole-program type a...
详细信息
The proceedings contains 26 papers from the fifth acm sigplan conference on principle and practice of declarative programming. The topics discussed include: a functional correspondence between evaluators and abstract ...
详细信息
ISBN:
(纸本)1581137052
The proceedings contains 26 papers from the fifth acm sigplan conference on principle and practice of declarative programming. The topics discussed include: a functional correspondence between evaluators and abstract machines;conditional narrowing without conditions;finding all minimal unsatisfiable subsets;formally deriving an STG machine;and refining weakly outermost-needed rewriting and narrowing.
We present a technique for cryptographic protocol verification, based on an intermediate representation of the protocol by a set of Horn clauses (a logic program). This technique makes it possible to verify security p...
详细信息
ISBN:
(纸本)1581137052
We present a technique for cryptographic protocol verification, based on an intermediate representation of the protocol by a set of Horn clauses (a logic program). This technique makes it possible to verify security properties of the protocols, such as secrecy and authenticity, in a fully automatic way. Furthermore, the obtained security proofs are valid for an unbounded number of sessions of the protocol.
This paper formalizes and proves correct a compilation scheme for mutually-recursive definitions in call-by-value functional languages. This scheme supports a wider range of recursive definitions than standard call-by...
详细信息
ISBN:
(纸本)1581137052
This paper formalizes and proves correct a compilation scheme for mutually-recursive definitions in call-by-value functional languages. This scheme supports a wider range of recursive definitions than standard call-by-value recursive definitions. We formalize our technique as a translation scheme to a lambda-calculus featuring in-place update of memory blocks, and prove the translation to be faithful.
Proof checkers for proof-carrying code (and similar systems) can suffer from two problems: huge proof witnesses and untrustworthy proof rules. No previous design has addressed both of these problems simultaneously. We...
详细信息
ISBN:
(纸本)1581137052
Proof checkers for proof-carrying code (and similar systems) can suffer from two problems: huge proof witnesses and untrustworthy proof rules. No previous design has addressed both of these problems simultaneously. We show the theory, design, and implementation of a proof-checker that permits small proof witnesses and machine-checkable proofs of the soundness of the system.
Non-strict purely functional languages pose many challenges to the designers of debugging tools. declarative debugging has long been considered a suitable candidate for the task due to its abstraction over the evaluat...
详细信息
ISBN:
(纸本)1581137052
Non-strict purely functional languages pose many challenges to the designers of debugging tools. declarative debugging has long been considered a suitable candidate for the task due to its abstraction over the evaluation order of the program, although the provision of practical implementations has been lagging. In this paper we discuss the solutions used in our declarative debugger for Haskell to tackle the problems of printing values, memory usage and I/O. The debugger is based on program transformation, although much leverage is gained by interfacing with the runtime environment of the language implementation through a foreign function interface.
In this paper we propose a semantically well-founded combination of the constraint solvers used in the constraint programming languages CLP (SET) and CLP(FD). This work demonstrates that it is possible to provide effi...
详细信息
ISBN:
(纸本)1581137052
In this paper we propose a semantically well-founded combination of the constraint solvers used in the constraint programming languages CLP (SET) and CLP(FD). This work demonstrates that it is possible to provide efficient executions (through CLP (FD) solvers) while maintaining the expressive power and flexibility of the CLP(SET) language. We develop a combined constraint solver and we show how static analysis can help in organizing the distribution of constraints to the two constraint solvers.
Language for Structured Design (LSD) is a high level, visual, logic programming language for design of structured objects. LSD combines the design and programming activities in a homogeneous programming/design environ...
详细信息
ISBN:
(纸本)1581137052
Language for Structured Design (LSD) is a high level, visual, logic programming language for design of structured objects. LSD combines the design and programming activities in a homogeneous programming/design environment by extending Lograph, a visual logic programming language, with the notion of solids and operations on them. At the back-end, however, a solid modeling kernel for maintaining low level description of solids and operations is required. In this paper, we report on our progress towards employing PLaSM, a functional programming language for solid modeling, as the solid modeling kernel of LSD. This is achieved through the use of a translator engine which transforms the high level object description produced by LSD programs to PLaSM programs.
In rule-based languages, control of rule application can be expressed thanks to strategy constructors. The paper addresses termination of such strategy-guided evaluation. To fix ideas, we use the ELAN strategy languag...
详细信息
ISBN:
(纸本)1581137052
In rule-based languages, control of rule application can be expressed thanks to strategy constructors. The paper addresses termination of such strategy-guided evaluation. To fix ideas, we use the ELAN strategy language. We first give a sufficient criterion for ELAN-like strategies to terminate, only lying on rewrite rules involved in the strategy. We then give a simplification process of strategies, itself described by rewriting, to empower the previous criterion. This simplification can also make proofs of other program properties easier.
暂无评论