Generic Type inference for the psi-calculi
Translated title
Generisk typeinferens for psi-kalkyler
Authors
Bjerregaard, Mathias Ormstrup ; Graversen, Eva Fajstrup
Term
4. term
Education
Publication year
2016
Submitted on
2016-06-09
Pages
102
Abstract
This thesis develops a generic, constraint-based type inference framework for the simple and linear type systems for ψ-calculi. The approach systematically translates typing rules for processes into constraint generation rules expressed in a decidable fragment of first-order logic, Alternation-Free Least Fixpoint Logic (ALFP). Instead of assigning concrete types in the typing environment, we use type variables and encode side conditions as constraints, so well-typedness reduces to solving the resulting constraint set. Because ψ-calculi and the generic type systems are parameterised by terms, assertions, and conditions, each instantiation must supply (i) constraint rules for these components and (ii) a fixed set of axioms that give meaning to the relations used in constraints; we state simple requirements on these axioms to ensure correctness. We outline a four-step procedure for instantiation (choose a ψ-calculus, instantiate the type system, derive constraint rules, and define relations and axioms) and prove soundness of the framework. The method is illustrated with instantiations for simply typed ψ-calculi (including explicit fusion and correspondence assertions) and linearly typed ψ-calculi (including simple linear types), and we discuss challenges that arise in more advanced settings, such as attempts to ensure termination for value-passing processes.
Dette speciale udvikler en generisk, konstraintbaseret typeinferensramme for de simple og lineære typesystemer for ψ-calculi. Metoden er at omsætte typeregler for processer til konstraintgenereringsregler og udtrykke dem i en afgørelig del af førsteordenslogik, den alternationsfri mindstefikspunktlogik (ALFP). I stedet for at tildele konkrete typer i typeomgivelser bruger vi typevariabler og koder sidebetingelser som konstraints, så spørgsmålet om veltypethed reduceres til at finde en løsning på konstraintsættet. Fordi ψ-calculi og de generiske typesystemer er parameteriserede af termer, assertioner og betingelser, skal hver instans levere (i) konstraintregler for disse komponenter og (ii) et fast sæt aksiomer, der giver de anvendte relationer deres betydning; vi angiver simple krav til disse, så inferensen er korrekt. Vi skitserer en firetrins fremgangsmåde til instansiering (valg af ψ-calculus, typesystem, afledning af konstraintregler samt definition af relationer og aksiomer) og beviser lydhed/korrekthed af rammen. Tilgangen illustreres med instanser for simpel typning (bl.a. eksplicit fusion og korrespondence-assertioner) og lineær typning (bl.a. simple lineære typer) og diskuteres i forhold til udfordringer ved mere avancerede systemer, herunder forsøg på at sikre terminering for værdioverførende processer.
[This apstract has been generated with the help of AI directly from the project full text]
Keywords