ICFP
2003
ACM
14 years 5 months ago
2003
ACM
In this paper we extend the model of program variables from the Refinement Calculus [2] in order to be able to reason more algebraically about recursive procedures with parameter...
ICFP
2003
ACM
15 years 11 days ago
2003
ACM
Under the widely believed conjecture P=NP, NP-complete problems cannot be solved exactly using efficient polynomial time algorithms. Furthermore, any instance of a NP-complete pro...
ICFP
2003
ACM
15 years 11 days ago
2003
ACM
I describe the mechanisation in HOL of some basic -calculus theory, using the axioms proposed by Gordon and Melham [4]. Using these as a foundation, I mechanised the proofs from C...
ICFP
2003
ACM
15 years 11 days ago
2003
ACM
We report on work in progress regarding a foundation for the notion of meta-variable in logical frameworks and type theories. Our proposal is to treat meta-variables as modal varia...
ICFP
2003
ACM
2003
ACM
A formalization of an Ordered Logical Framework in Hybrid with applications to continuation machines
15 years 11 days ago
We report on work in progress devoted to the formalization of an Ordered Logical Framework (OLF) based on a two-level architecture [8] in the Hybrid system. OLF here is a second-or...
ICFP
2003
ACM
15 years 11 days ago
2003
ACM
We have verified several versions of the CPS transformation in Isabelle/HOL. In our verification we adopted first-order abstract syntax with variable names so that the formalizati...
ICFP
2003
ACM
15 years 11 days ago
2003
ACM
The task of designing and implementing a compiler can be a difficult and error-prone process. In this paper, we present proach based on the use of higher-order abstract syntax and...
ICFP
2003
ACM
15 years 11 days ago
2003
ACM
ICFP
2003
ACM
15 years 11 days ago
2003
ACM
ICFP
2003
ACM
15 years 11 days ago
2003
ACM
