Export Citations
Save this search
Please login to be able to save your searches and receive alerts for new content matching your search criteria.
- ArticleAugust 2003
Foundational proof checkers with small witnesses
PPDP '03: Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programmingPages 264–274https://doi.org/10.1145/888251.888276Proof 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 ...
- ArticleAugust 2003
Practical aspects of declarative debugging in Haskell 98
PPDP '03: Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programmingPages 230–240https://doi.org/10.1145/888251.888273Non-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 ...
- ArticleAugust 2003
Simplification and termination of strategies in rule-based languages
PPDP '03: Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programmingPages 124–135https://doi.org/10.1145/888251.888264In 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 ...
- ArticleAugust 2003
Statically assuring secrecy for dynamic concurrent processes
PPDP '03: Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programmingPages 91–101https://doi.org/10.1145/888251.888261We propose a new algorithm of secrecy analysis in a framework integrating declarative programming and concurrency. The analysis of a program ensures that information can only flow from less sensitive levels toward more sensitive ones. Our algorithm uses ...
- ArticleAugust 2003
ViMer: a visual debugger for mercury
PPDP '03: Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programmingPages 56–66https://doi.org/10.1145/888251.888258ViMer is a visual debugging environment for Mercury programs which has three main contributions. First, it employs a new execution tree representation, the layered AND-OR tree, which we believe provides a better way of visualizing backtracking in AND-OR-...
- ArticleAugust 2003
Automatic verification of cryptographic protocols: a logic programming approach
PPDP '03: Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programmingPages 1–3https://doi.org/10.1145/888251.888252We 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 ...