Docteur En Informatique, Boris Yakobowski, Roberto Di Cosmo, Stéphanie Weirich, Hugo Herbelin, ...
pour obtenir le titre de
Boris Yakobowski, Roberto Di Cosmo, Stéphanie Weirich, Hugo Herbelin, Fritz Henglein, ...
présentée à
IOS Press Coinductive Axiomatization of Recursive Type Equality and Subtyping (2007)
Michael Brandt, Fritz Henglein
Abstract. We present new sound and complete axiomatizations of type equality and subtype inequality for a first-order type language with regular recursive types. The rules are motivated by...
AnnoDomini in Practice: A Type-Theoretic Approach to the Year 2000 Problem (2007)
Peter Harry Eidorff, Fritz Henglein, Christian Mossin, Peter Harry, Eidorff Fritz, Henglein Christian Mossin, ...
. AnnoDomini is a commercially available source-to-source conversion tool for finding and fixing Year 2000 problems in COBOL programs. AnnoDomini uses type-based specification, analysis, and...
Breaking through the n³ barrier: Faster object type inference (2007)
this paper we improve each one of the four type inference problems from O(n
Barrier Faster, Fritz Henglein
Abadi and Cardelli [AC96] have presented and investigated object calculi that model most object-oriented features found in actual objectoriented programming languages. The calculi are innate object...
Fritz Henglein, Henning Makholm, Henning Niss
A direct approach to control-flow sensitive
Fritz Henglein, Henning Makholm, Henning Niss
A direct approach to control-flow sensitive
the Principles of Programming Lnguages (POPL 99), 1999. (2007)
Order Mads Tofte, M. Tofte, L. Birkedal, M. Elsman, Mads Tofte, Gordon Plotkin, ...
Publications and notes in chronological
Jesper Andersen, Ebbe Elsborg, Fritz Henglein, Jakob Grue, Simonsen Christian Stefansen, J. Andersen, ...
Abstract We present a declarative language for compositional specification of contracts governing the exchange of resources. It extends Eber and Peyton Jones’s declarative language for specifying...
Morten Bartvig, Peter Theill, Fritz Henglein
This thesis proposes a method for implementing authorization in XML Store. It is shown that access control can be implemented using XML Store’s value-oriented model without affecting the XML Store...
Multiset discrimination (2003)
Multiset discrimination is a fundamental technique for finding duplicates in linear time without hashing or comparison-based sorting. It can be viewed as a generalization of equality (or equivalence)...
E.: Compositional specification of commercial contracts. M.S. term project (2003)
Jesper Andersen, Ebbe Elsborg, Fritz Henglein, Jakob Grue Simonsen
Abstract. We present a declarative language for compositional specification of contracts governing the exchange of resources. It extends Eber and Peyton Jones’s declarative language for specifying...
E.: Compositional specification of commercial contracts. M.S. term project (2003)
Jesper Andersen, Ebbe Elsborg, Fritz Henglein, Jakob Grue Simonsen
Abstract. We present a declarative language for compositional specification of contracts governing the exchange of resources. It extends Eber and Peyton Jones’s declarative language for specifying...
IT-University of Copenhagen (2002)
Kasper Bøgebjerg Pedersen, Jesper Tejlgaard Pedersen, Michael R. Hansen, Fritz Henglein
This thesis presents a distributed value-oriented storage facility for storing XML documents called XML Store. XML documents stored in XML Store can be accessed and manipulated using an API, called...
Simon Helsen, Dekan Prof, Dr. Thomas Ottmann, Erstreferent Prof, Dr. Peter Thiemann, ...
des Quellprogramms statisch, also wenig veränderlich ist; denn partielle Auswerter spezialisieren Programme, indem sie möglichst viele Operationen durch das aggressive Weiterleiten von Konstanten...
AnnoDomini: From Type Theory to Year 2000 Conversion Tool (1999)
Peter Harry Eidorff, Fritz Henglein, Christian Mossin, Peter Harry, Eidorff Fritz, Mads Tofte, ...
AnnoDomini is a source-to-source conversion tool for making COBOL programs Year 2000 compliant. It is technically and conceptually built upon type-theoretic techniques and methods: type-based...
Coinductive Axiomatization of Recursive Type Equality and Subtyping (1998)
Michael Brandt, Fritz Henglein
. We present new sound and complete axiomatizations of type equality and subtype inequality for a first-order type language with regular recursive types. The rules are motivated by coinductive...
Constraint Automata and the Complexity of Recursive Subtype Entailment (1998)
. We study entailment of structural and nonstructural recursive subtyping constraints. Constraints are formal inequalities between type expressions, interpreted over an ordered set of possibly...
The Complexity of Subtype Entailment for Simple Types (1997)
A subtyping 0 is entailed by a set of subtyping constraints C, written C j= 0 , if every valuation (mapping of type variables to ground types) that satisfies C also satisfies 0 . We study the...
Coinductive Axiomatization of Recursive Type Equality and Subtyping (1997)
Michael Brandt, Fritz Henglein
. We present new sound and complete axiomatizations of type equality and subtype inequality for a first-order type language with regular recursive types. The rules are motivated by coinductive...
Syntactic Properties of Polymorphic Subtyping (1996)
Subtyping is used in language design, type checking and program analysis. Mitchell and others have studied the foundations of structural subtyping (primitive subtype relations only between type...
Breaking through the n³ barrier: Faster object type inference (1996)
Abadi and Cardelli [AC96] have presented and investigated object calculi that model most object-oriented features found in actual objectoriented programming languages. The calculi are innate object...
A Semantic Model of Binding Times for Safe Partial Evaluation (1995)
In program optimisation an analysis determines some information about a portion of a program, which is then used to justify certain transformations on the code. The correctness of the optimisation...
Safe polymorphic type inference for a Dynamically Typed Language: Translating Scheme to ML (1995)
We describe a new method for polymorphic type inference for the dynamically typed language Scheme. The method infers both types and explicit run-time type operations (coercions) for a given program....
A Semantic Model of Binding Times for Safe Partial Evaluation (1995)
In program optimisation an analysis determines some information about a portion of a program, which is then used to justify certain transformations on the code. The correctness of the optimisation...
Global Tagging Optimization by Type Inference (1992)
Tag handling accounts for a substantial amount of execution cost in latently typed languages such as Common LISP and Scheme, especially on architectures that provide no special hardware support. We...
Efficient Type Inference for Higher-Order Binding-Time Analysis (1991)
Binding-time analysis determines when variables and expressions in a program can be bound to their values, distinguishing between early (compile-time) and late (run-time) binding. Binding-time...
Programming with Structures, Functions, and Objects (1991)
Fritz Henglein, Konstantin Läufer
We describe program structuring mechanisms for integrating algebraic, functional and objectoriented programming in a single framework. Our language is a statically typed higher-order language with...
Programming with Structures, Functions, and Objects (1991)
Fritz Henglein, Konstantin Läufer
We describe program structuring mechanisms for integrating algebraic, functional and objectoriented programming in a single framework. Our language is a statically typed higher-order language with...
Type Inference with Polymorphic Recursion (1991)
The Damas-Milner Calculus is the typed -calculus underlying the type system for ML and several other strongly typed polymorphic functional languages such as Miranda 1 and Haskell. Mycroft has...
Efficient Type Inference for Higher-Order Binding-Time Analysis (1991)
Binding-time analysis determines when variables and expressions in a program can be bound to their values, distinguishing between early (compile-time) and late (run-time) binding. Binding-time...
The Complexity of Type Inference for Higher-Order Typed Lambda Calculi (1991)
Fritz Henglein, Harry G. Mairson
We analyze the computational complexity of type inference for untyped -terms in the second-order polymorphic typed -calculus (F 2 ) invented by Girard and Reynolds, as well as higher-order extensions...
Polymorphic Type Inference and Semi-Unification (1989)
In the last ten years declaration-free programming languages with a polymorphic typing discipline (ML, B) have been developed to approximate the flexibility and conciseness of dynamically typed...