Sciweavers

Share
warning: Creating default object from empty value in /var/www/modules/taxonomy/taxonomy.module on line 1416.
TYPES
2004
Springer
10 years 6 months ago
Tactic-Based Optimized Compilation of Functional Programs
Abstract Within a framework of correct code-generation from HOLspecifications, we present a particular instance concerned with the optimized compilation of a lazy language (called...
Thomas Meyer, Burkhart Wolff
TYPES
2004
Springer
10 years 6 months ago
A Few Constructions on Constructors
We present four constructions for standard equipment which can be generated for every inductive datatype: case analysis, structural recursion, no confusion, acyclicity. Our constru...
Conor McBride, Healfdene Goguen, James McKinna
TYPES
2004
Springer
10 years 6 months ago
Surreal Numbers in Coq
Lionel Elie Mamane
TYPES
2004
Springer
10 years 6 months ago
A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis
Yves Bertot, Benjamin Grégoire, Xavier Lero...
TYPES
2004
Springer
10 years 6 months ago
Extracting a Normalization Algorithm in Isabelle/HOL
We present a formalization of a constructive proof of weak normalization for the simply-typed λ-calculus in the theorem prover Isabelle/HOL, and show how a program can be extracte...
Stefan Berghofer
TYPES
2004
Springer
10 years 6 months ago
A Machine-Checked Formalization of the Random Oracle Model
Abstract. Most approaches to the formal analysis of cryptography protocols make the perfect cryptographic assumption, which entails for example that there is no way to obtain knowl...
Gilles Barthe, Sabrina Tarento
TYPES
2004
Springer
10 years 6 months ago
A Content Based Mathematical Search Engine: Whelp
Abstract. The prototype of a content based search engine for mathematical knowledge supporting a small set of queries requiring matching and/or typing operations is described. The ...
Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti...
TYPES
2004
Springer
10 years 6 months ago
Exploring the Regular Tree Types
In this paper we use the Epigram language to define the universe of regular tree types—closed under empty, unit, sum, product and least fixpoint. We then present a generic deci...
Peter Morris, Thorsten Altenkirch, Conor McBride
books