AISC
2008
Springer
14 years 1 months ago
2008
Springer
Abstract. Assumptions about the domains of partial functions are necessary in state-of-the-art proof assistants. On the other hand when mathematicians write about partial functions...
TACAS
2000
Springer
14 years 3 months ago
2000
Springer
This note describes Proof General, a tool for developing machine proofs with an interactive proof assistant. Interaction is based around a proof script, which is the target of a pr...
FROCOS
2007
Springer
14 years 3 months ago
2007
Springer
Abstract. Nowadays, formal methods rely on tools of different kinds: proof assistants with which the user interacts to discover a proof step by step; and fully automated tools whic...
CCS
2004
ACM
14 years 4 months ago
2004
ACM
Information flow type systems provide an elegant means to enforce confidentiality of programs. Using the proof assistant Isabelle/HOL, we have machine-checked a recent work of B...
EUROCAST
2005
Springer
14 years 5 months ago
2005
Springer
In this paper, an approach to synthesize correct programs from specifications is presented. The idea is to extract code from definitions appearing in statements which have been me...
HASKELL
2005
ACM
14 years 5 months ago
2005
ACM
Proof assistants based on dependent type theory are closely related to functional programming languages, and so it is tempting to use them to prove the correctness of functional p...
TPHOL
2006
IEEE
14 years 5 months ago
2006
IEEE
Abstract. We compare the styles of several proof assistants for mathematics. We present Pythagoras’ proof of the irrationality of √ 2 both informal and formalized in (1) HOL, (...
PROVSEC
2007
Springer
14 years 5 months ago
2007
Springer
Game-playing is an approach to write security proofs that are easy to verify. In this approach, security definitions and intractable problems are written as programs called games ...
ICICS
2007
Springer
14 years 5 months ago
2007
Springer
Abstract. To be accepted, a cryptographic scheme must come with a proof that it satisfies some standard security properties. However, because cryptographic schemes are based on no...
CEFP
2007
Springer
14 years 5 months ago
2007
Springer
This tutorial paper aims to provide the necessary expertise for working with the proof assistant Sparkle, which is dedicated to the lazy functional programming language Clean. The ...