publications: - title: "Polymorphic Binding-Time Analysis" author: - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" - name: "Christian Mossin" link: "https://researchr.org/alias/christian-mossin" year: "1994" doi: "http://www.springerlink.com/content/p8g505w5304226t7/" abstract: "Binding time analysis is an important part of off-line partial evaluation, annotating expressions as being safely evaluable from known data or possibly depending on unknown data. Most binding-time analyses have been monovariant, allowing only one binding-time description for each function. The idea of polyvariance is to allow multiple binding time descriptions of each function, by duplicating the function [6, 2] or by associating a set of binding time descriptions to each function [3]. Instead we present an inference based binding time analysis polymorphic in binding time values. This polymorphism captures a very powerful notion of polyvariance limited only by the (standard) types of the language. Polymorphism gives a much simpler definition than the known polyvariant schemes allowing us to reason formally about the system and prove it correct. This paper is based on work in [14]. " links: doi: "http://www.springerlink.com/content/p8g505w5304226t7/" tags: - "type inference" - "rule-based" - "data-flow language" - "analysis" - "type system" - "binding-time" - "data-flow" - "partial evaluation" - "data-flow analysis" researchr: "https://researchr.org/publication/HengleinM94%3A0" cites: 0 citedby: 0 pages: "287-301" booktitle: "ESOP" kind: "inproceedings" key: "HengleinM94:0" - title: "Compositional specification of commercial contracts" author: - name: "Jesper Andersen" link: "https://researchr.org/alias/jesper-andersen" - name: "Ebbe Elsborg" link: "https://researchr.org/alias/ebbe-elsborg" - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" - name: "Jakob Grue Simonsen" link: "https://researchr.org/alias/jakob-grue-simonsen" - name: "Christian Stefansen" link: "https://researchr.org/alias/christian-stefansen" year: "2006" doi: "http://dx.doi.org/10.1007/s10009-006-0010-1" links: doi: "http://dx.doi.org/10.1007/s10009-006-0010-1" tags: - "contracts" - "composition" researchr: "https://researchr.org/publication/AndersenEHSS06" cites: 0 citedby: 0 journal: "STTT" volume: "8" number: "6" pages: "485-516" kind: "article" key: "AndersenEHSS06" - title: "SIGPLAN and the World Series" author: - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" year: "1998" researchr: "https://researchr.org/publication/Henglein98" cites: 0 citedby: 0 journal: "SIGPLAN" volume: "33" number: "1" pages: "1-2" kind: "article" key: "Henglein98" - title: "Mechanical Translation of Set Theoretic Problem Specifications into Efficient RAM Code-A Case Study" author: - name: "Robert Paige" link: "https://researchr.org/alias/robert-paige" - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" year: "1987" tags: - "translation" - "case study" researchr: "https://researchr.org/publication/PaigeH87" cites: 0 citedby: 0 journal: "JSC" volume: "4" number: "2" pages: "207-232" kind: "article" key: "PaigeH87" - title: "Optimizing Relational Algebra Operations Using Generic Equivalence Discriminators and Lazy Products" author: - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" tags: - "laziness" - "optimization" - "relational algebra" - " algebra" researchr: "https://researchr.org/publication/Henglein%3APEPM%3A2010" cites: 0 citedby: 0 booktitle: "PEPM" kind: "inproceedings" key: "Henglein:PEPM:2010" - title: "Type Inference and Semi-Unification" author: - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" year: "1988" doi: "http://doi.acm.org/10.1145/62678.62701" links: doi: "http://doi.acm.org/10.1145/62678.62701" tags: - "type inference" researchr: "https://researchr.org/publication/Henglein88" cites: 0 citedby: 0 pages: "184-197" booktitle: "lfp" kind: "inproceedings" key: "Henglein88" - title: "Type Inference with Polymorphic Recursion" author: - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" year: "1993" doi: "http://doi.acm.org/10.1145/169701.169692" links: doi: "http://doi.acm.org/10.1145/169701.169692" tags: - "type inference" researchr: "https://researchr.org/publication/Henglein93" cites: 0 citedby: 0 journal: "TOPLAS" volume: "15" number: "2" pages: "253-289" kind: "article" key: "Henglein93" - title: "Optimizing relational algebra operations using generic equivalence discriminators and lazy products" author: - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" year: "2010" doi: "http://doi.acm.org/10.1145/1706356.1706372" links: doi: "http://doi.acm.org/10.1145/1706356.1706372" tags: - "laziness" - "optimization" - "relational algebra" - " algebra" researchr: "https://researchr.org/publication/Henglein10" cites: 0 citedby: 0 pages: "73-82" booktitle: "PEPM" kind: "inproceedings" key: "Henglein10" - title: "Compositional Specification of Commercial Contracts" author: - name: "Jesper Andersen" link: "https://researchr.org/alias/jesper-andersen" - name: "Ebbe Elsborg" link: "https://researchr.org/alias/ebbe-elsborg" - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" - name: "Jakob Grue Simonsen" link: "https://researchr.org/alias/jakob-grue-simonsen" - name: "Christian Stefansen" link: "https://researchr.org/alias/christian-stefansen" year: "2004" tags: - "contracts" - "composition" researchr: "https://researchr.org/publication/AndersenEHSS04" cites: 0 citedby: 0 pages: "103-110" booktitle: "ISoLA" kind: "inproceedings" key: "AndersenEHSS04" - title: "Coinductive Axiomatization of Recursive Type Equality and Subtyping" author: - name: "Michael Brandt" link: "https://researchr.org/alias/michael-brandt" - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" year: "1997" tags: - "subtyping" researchr: "https://researchr.org/publication/BrandtH97" cites: 0 citedby: 0 pages: "63-81" booktitle: "tlca" kind: "inproceedings" key: "BrandtH97" - title: "Coinductive Axiomatization of Recursive Type Equality and Subtyping" author: - name: "Michael Brandt" link: "https://researchr.org/alias/michael-brandt" - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" year: "1998" tags: - "subtyping" researchr: "https://researchr.org/publication/BrandtH98" cites: 0 citedby: 0 journal: "FUIN" volume: "33" number: "4" pages: "309-338" kind: "article" key: "BrandtH98" - title: "Editorial" author: - name: "Olivier Danvy" link: "https://www.yale-nus.edu.sg/about/faculty/olivier-danvy/" - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" - name: "Harry G. Mairson" link: "https://researchr.org/alias/harry-g.-mairson" - name: "Alberto Pettorossi" link: "https://researchr.org/alias/alberto-pettorossi" year: "2005" doi: "http://dx.doi.org/10.1007/s10990-005-7001-x" links: doi: "http://dx.doi.org/10.1007/s10990-005-7001-x" researchr: "https://researchr.org/publication/DanvyHMP05" cites: 0 citedby: 0 journal: "lisp" volume: "18" number: "1-2" pages: "5-6" kind: "article" key: "DanvyHMP05" - title: "Polymorphic Recursion and Subtype Qualifications: Polymorphic Binding-Time Analysis in Polynomial Time" author: - name: "Dirk Dussart" link: "https://researchr.org/alias/dirk-dussart" - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" - name: "Christian Mossin" link: "https://researchr.org/alias/christian-mossin" year: "1995" tags: - "analysis" - "subtyping" researchr: "https://researchr.org/publication/DussartHM95" cites: 0 citedby: 0 pages: "118-135" booktitle: "SAS" kind: "inproceedings" key: "DussartHM95" - title: "AnnoDomini: From Type Theory to Year 2000 Conversion Tool" author: - name: "Peter Harry Eidorff" link: "https://researchr.org/alias/peter-harry-eidorff" - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" - name: "Christian Mossin" link: "https://researchr.org/alias/christian-mossin" - name: "Henning Niss" link: "https://researchr.org/alias/henning-niss" - name: "Morten Heine Sørensen" link: "https://researchr.org/alias/morten-heine-s%C3%B8rensen" - name: "Mads Tofte" link: "https://researchr.org/alias/mads-tofte" year: "1999" doi: "http://doi.acm.org/10.1145/292540.292543" links: doi: "http://doi.acm.org/10.1145/292540.292543" tags: - "type theory" researchr: "https://researchr.org/publication/EidorffHMNST99" cites: 0 citedby: 0 pages: "1-14" booktitle: "POPL" kind: "inproceedings" key: "EidorffHMNST99" - title: "The Complexity of Type Inference for Higher-Order Typed Lambda Calculi" author: - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" - name: "Harry G. Mairson" link: "https://researchr.org/alias/harry-g.-mairson" year: "1991" tags: - "type inference" researchr: "https://researchr.org/publication/HengleinM91" cites: 0 citedby: 0 pages: "119-130" booktitle: "POPL" kind: "inproceedings" key: "HengleinM91" - title: "What is a Sorting Function?" author: - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" year: "2009" doi: "http://dx.doi.org/10.1016/j.jlap.2008.12.003" links: doi: "http://dx.doi.org/10.1016/j.jlap.2008.12.003" researchr: "https://researchr.org/publication/Henglein09" cites: 0 citedby: 0 journal: "jlp" volume: "78" number: "7" pages: "552-572" kind: "article" key: "Henglein09" - title: "The Complexity of Subtype Entailment for Simple Types" author: - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" - name: "Jakob Rehof" link: "https://researchr.org/alias/jakob-rehof" year: "1997" doi: "http://www.computer.org/proceedings/lics/7925/79250352abs.htm" links: doi: "http://www.computer.org/proceedings/lics/7925/79250352abs.htm" tags: - "subtyping" researchr: "https://researchr.org/publication/HengleinR97" cites: 0 citedby: 0 pages: "352-361" booktitle: "lics" kind: "inproceedings" key: "HengleinR97" - title: "Breaking Through the n:::3::: Barrier: Faster Object Type Inference" author: - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" year: "1999" tags: - "type inference" researchr: "https://researchr.org/publication/Henglein99" cites: 0 citedby: 0 journal: "tapos" volume: "5" number: "1" pages: "57-72" kind: "article" key: "Henglein99" - title: "Dynamic Typing: Syntax and Proof Theory" author: - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" year: "1994" tags: - "type theory" researchr: "https://researchr.org/publication/Henglein94" cites: 0 citedby: 0 journal: "SCP" volume: "22" number: "3" pages: "197-230" kind: "article" key: "Henglein94" - title: "Fast Left-Linear Semi-Unification" author: - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" year: "1990" researchr: "https://researchr.org/publication/Henglein90" cites: 0 citedby: 0 pages: "82-91" booktitle: "icci" kind: "inproceedings" key: "Henglein90" - title: "Generic discrimination: sorting and paritioning unshared data in linear time" author: - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" year: "2008" doi: "http://doi.acm.org/10.1145/1411204.1411220" links: doi: "http://doi.acm.org/10.1145/1411204.1411220" tags: - "data-flow" researchr: "https://researchr.org/publication/Henglein08" cites: 0 citedby: 0 pages: "91-102" booktitle: "ICFP" kind: "inproceedings" key: "Henglein08" - title: "POETS: Process-oriented event-driven transaction systems" author: - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" - name: "Ken Friis Larsen" link: "https://researchr.org/alias/ken-friis-larsen" - name: "Jakob Grue Simonsen" link: "https://researchr.org/alias/jakob-grue-simonsen" - name: "Christian Stefansen" link: "https://researchr.org/alias/christian-stefansen" year: "2009" doi: "http://dx.doi.org/10.1016/j.jlap.2008.08.007" links: doi: "http://dx.doi.org/10.1016/j.jlap.2008.08.007" researchr: "https://researchr.org/publication/HengleinLSS09" cites: 0 citedby: 0 journal: "jlp" volume: "78" number: "5" pages: "381-401" kind: "article" key: "HengleinLSS09" - title: "A Decidable Case of the Semi-Unification Problem" author: - name: "Hans Leiß" link: "https://researchr.org/alias/hans-lei%C3%9F" - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" year: "1991" researchr: "https://researchr.org/publication/LeissH91" cites: 0 citedby: 0 pages: "318-327" booktitle: "mfcs" kind: "inproceedings" key: "LeissH91" - title: "AnnoDomini in Practice: A Type-Theoretic Approach to the Year 2000 Problem" author: - name: "Peter Harry Eidorff" link: "https://researchr.org/alias/peter-harry-eidorff" - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" - name: "Christian Mossin" link: "https://researchr.org/alias/christian-mossin" - name: "Henning Niss" link: "https://researchr.org/alias/henning-niss" - name: "Morten Heine Sørensen" link: "https://researchr.org/alias/morten-heine-s%C3%B8rensen" - name: "Mads Tofte" link: "https://researchr.org/alias/mads-tofte" year: "1999" doi: "http://link.springer.de/link/service/series/0558/bibs/1581/15810006.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/1581/15810006.htm" tags: - "systematic-approach" researchr: "https://researchr.org/publication/EidorffHMNST99%3A0" cites: 0 citedby: 0 pages: "6-13" booktitle: "tlca" kind: "inproceedings" key: "EidorffHMNST99:0" - title: "Mechanical Translation of Set Theoretic Problem Specifications into Efficient RAM Code - A Case Study" author: - name: "Robert Paige" link: "https://researchr.org/alias/robert-paige" - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" year: "1985" tags: - "translation" - "case study" researchr: "https://researchr.org/publication/PaigeH85" cites: 0 citedby: 0 pages: "554-567" booktitle: "eurocal" kind: "inproceedings" key: "PaigeH85" - title: "A Semantic Model of Binding Times for Safe Partial Evaluation" author: - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" - name: "David Sands" link: "https://researchr.org/alias/david-sands" year: "1995" tags: - "partial evaluation" researchr: "https://researchr.org/publication/HengleinS95" cites: 0 citedby: 0 pages: "299-320" booktitle: "plilp" kind: "inproceedings" key: "HengleinS95" - title: "Global Tagging Optimization by Type Inference" author: - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" year: "1992" doi: "http://doi.acm.org/10.1145/141471.141542" links: doi: "http://doi.acm.org/10.1145/141471.141542" tags: - "optimization" - "type inference" - "tagging" researchr: "https://researchr.org/publication/Henglein92" cites: 0 citedby: 0 pages: "205-215" booktitle: "lfp" kind: "inproceedings" key: "Henglein92" - title: "A Direct Approach to Control-Flow Sensitive Region-Based Memory Management" author: - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" - name: "Henning Makholm" link: "https://researchr.org/alias/henning-makholm" - name: "Henning Niss" link: "https://researchr.org/alias/henning-niss" year: "2001" tags: - "rule-based" - "memory management" - "data-flow" - "systematic-approach" researchr: "https://researchr.org/publication/HengleinMN01" cites: 0 citedby: 0 pages: "175-186" booktitle: "ppdp" kind: "inproceedings" key: "HengleinMN01" - title: "Iterative Fixed Point Computation for Type-Based Strictness Analysis" author: - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" year: "1994" tags: - "rule-based" - "analysis" researchr: "https://researchr.org/publication/Henglein94%3A0" cites: 0 citedby: 0 pages: "395-407" booktitle: "SAS" kind: "inproceedings" key: "Henglein94:0" - title: "Constraint Automata and the Complexity of Recursive Subtype Entailment" author: - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" - name: "Jakob Rehof" link: "https://researchr.org/alias/jakob-rehof" year: "1998" doi: "http://link.springer.de/link/service/series/0558/bibs/1443/14430616.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/1443/14430616.htm" tags: - "constraints" - "subtyping" researchr: "https://researchr.org/publication/HengleinR98" cites: 0 citedby: 0 pages: "616-627" booktitle: "icalp" kind: "inproceedings" key: "HengleinR98" - title: "Editorial: Special Issue Dedicated to Bob Paige" author: - name: "Olivier Danvy" link: "https://www.yale-nus.edu.sg/about/faculty/olivier-danvy/" - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" - name: "Harry G. Mairson" link: "https://researchr.org/alias/harry-g.-mairson" - name: "Alberto Pettorossi" link: "https://researchr.org/alias/alberto-pettorossi" year: "2003" doi: "http://dx.doi.org/10.1023/A:1023059701827" links: doi: "http://dx.doi.org/10.1023/A:1023059701827" researchr: "https://researchr.org/publication/DanvyHMP03" cites: 0 citedby: 0 journal: "lisp" volume: "16" number: "1-2" pages: "5-6" kind: "article" key: "DanvyHMP03" - title: "Efficient Type Inference for Higher-Order Binding-Time Analysis" author: - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" year: "1991" doi: "http://www.springerlink.com/content/y255468h30456660/" abstract: "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 information can be used by compilers to produce more efficient target programs by partially evaluating programs at compile-time. Binding-time analysis has been formulated in abstract interpretation contexts and more recently in a type-theoretic setting. In a type-theoretic setting binding-time analysis is a type inference problem: the problem of inferring a completion of a -term e with binding-time annotations such that e satisfies the typing rules. Nielson and Nielson and Schmidt have shown that every simply typed -term has a unique completion ê that minimizes late binding in TML, a monomorphic type system with explicit binding-time annotations, and they present exponential time algorithms for computing such minimal completions. Gomard proves the same results for a variant of his two-level -calculus without a so-called lifting rule. He presents another algorithm for inferring completions in this somewhat restricted type system and states that it can be implemented in time O(n 3). He conjectures that the completions computed are minimal. In this paper we expand and improve on Gomard's work in the following ways. We identify the combinatorial core of type inference for binding-time analysis in Gomard's type system with lifting by effectively characterizing it as solving a specific class of constraints on type expressions. We present normalizing transformations on these constraints that preserve their solution sets, and we use the resultant normal forms to prove constructively the existence of minimal solutions, which yield minimal completions; this sharpens the minimal completion result of Gomard and extends it to the full type system with lifting. We devise a very efficient algorithm for computing minimal completions. It is a refinement of a fast unification algorithm, and an amortization argument shows that a fast union/find-based implementation executes in almost-linear time, O(n(n, n)), where is an inverse of Ackermann's function. Our results are for the two-level type system of Gomard, but we believe they are also adaptable to the Nielsons' TML. Our algorithm improves the computational complexity of computing minimal completions from exponential time to almost-linear time. It also improves on Gomard's polynomial time completion algorithm by a quadratic factor and as such appears to be the first efficient algorithm that provably computes minimal completions." links: doi: "http://www.springerlink.com/content/y255468h30456660/" tags: - "type inference" - "rule-based" - "program analysis" - "variable binding" - "refinement" - "analysis" - "constraints" - "type system" - "binding-time" - "rules" - "transformation system" - "e-science" - "compiler" - "context-aware" - "higher-order transformations" - "transformation" - "program transformation" researchr: "https://researchr.org/publication/Henglein91" cites: 0 citedby: 0 pages: "448-472" booktitle: "fpca" kind: "inproceedings" key: "Henglein91" - title: "Formally Optimal Boxing" author: - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" - name: "Jesper Jørgensen" link: "https://researchr.org/alias/jesper-j%C3%B8rgensen" year: "1994" researchr: "https://researchr.org/publication/HengleinJ94" cites: 0 citedby: 0 pages: "213-226" booktitle: "POPL" kind: "inproceedings" key: "HengleinJ94" - title: "The Complexity of Type Inference for Higher-Order Typed lambda Calculi" author: - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" - name: "Harry G. Mairson" link: "https://researchr.org/alias/harry-g.-mairson" year: "1994" tags: - "type inference" researchr: "https://researchr.org/publication/HengleinM94" cites: 0 citedby: 0 journal: "JFP" volume: "4" number: "4" pages: "435-477" kind: "article" key: "HengleinM94" - title: "Dynamic Typing" author: - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" year: "1992" researchr: "https://researchr.org/publication/Henglein92%3A0" cites: 0 citedby: 0 pages: "233-253" booktitle: "ESOP" kind: "inproceedings" key: "Henglein92:0" - title: "Safe Polymorphic Type Inference for Scheme: Translating Scheme to ML" author: - name: "Fritz Henglein" link: "http://www.diku.dk/hjemmesider/ansatte/henglein/" - name: "Jakob Rehof" link: "https://researchr.org/alias/jakob-rehof" year: "1995" tags: - "type inference" - "translation" researchr: "https://researchr.org/publication/HengleinR95" cites: 0 citedby: 0 pages: "192-203" booktitle: "fpca" kind: "inproceedings" key: "HengleinR95"