TLCA
2005
Springer
14 years 6 months ago
2005
Springer
We use a fully abstract denotational model to show that nested function calls and recursive definitions can be eliminated from SPCF (a typed functional language with simple non-lo...
TLCA
2005
Springer
14 years 6 months ago
2005
Springer
In a series of articles, we developed a method to translate general recursive functions written in a functional programming style into constructive type theory. Three problems rema...
TLCA
2005
Springer
14 years 6 months ago
2005
Springer
TLCA
2005
Springer
14 years 6 months ago
2005
Springer
Cut elimination is a central result of the proof theory. This paper proposes a new approach for proving the theorem for Gentzen’s intuitionistic sequent calculus LJ, that relies ...
TLCA
2005
Springer
14 years 6 months ago
2005
Springer
We give a monadic semantics in the category of FM-cpos to a higher-order CBV language with recursion and dynamically allocated mutable references that may store both ground data an...
TLCA
2005
Springer
14 years 6 months ago
2005
Springer
Proof animation is a way of executing proofs to nd errors in the formalization of proofs. It is intended to be \testing in proof engineering". Although the realizability inter...
TLCA
2005
Springer
14 years 6 months ago
2005
Springer
There is growing public concern about personal data collected by both private and public sectors. People have very little control over what kinds of data are stored and how such da...