Sökning: "parametricity"

Visar resultat 1 - 5 av 8 avhandlingar innehållade ordet parametricity.

1. 1. Internalizing Parametricity

   Författare :Guilhem Moulin; Chalmers tekniska högskola; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Type structure; Presheaf Model; Parametricity; Lambda Calculus; Polymorphism;

   Sammanfattning : Parametricity results have recently been proved for dependently-typed calculi such as the Calculus of Constructions. However these results are meta theorems, and although the theorems can be stated as internal propositions, they cannot be proved internally. LÄS MER

3. 2. Pure Type Systems with an Internalized Parametricity Theorem

   Författare :Guilhem Moulin; Chalmers tekniska högskola; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Type structure; Polymorphism; Lambda Calculus.; Parametricity;

   Sammanfattning : Parametricity results have recently been proved for dependently-typed calculi such as the Calculus of Constructions. However these results are meta theorems, and although they can be stated as internal propositions, they cannot be proved internally. LÄS MER

4. 3. Language-Based Differential Privacy with Accuracy Estimations and Sensitivity Analyses

   Författare :Elisabet Lobo Vesga; Chalmers tekniska högskola; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; haskell; accuracy; parametricity; Program reasoning; Functional Programming; concentration bounds; differential privacy;

   Sammanfattning : This thesis focuses on the development of programming frameworks to enforce, by construction, desirable properties of software systems. Particularly, we are interested in enforcing differential privacy -- a mathematical notion of data privacy -- while statically reasoning about the accuracy of computations, along with deriving the sensitivity of arbitrary functions to further strengthen the expressiveness of these systems. LÄS MER

5. 4. On the Foundations of Practical Language-Based Security

   Författare :Maximilian Algehed; Chalmers tekniska högskola; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Secure Multi-Execution; Parametricity; Programming Languages; Security;

   Sammanfattning : Language-based information flow control (IFC) promises to provide programming languages and tools that make it easy for developers to write secure code. Traditionally, research in this field aims to build a variant on a programming language or system that lets developers write code that gives them strong guarantees beyond the potential memory- and type-safety guarantees of modern languages. LÄS MER

7. 5. On Induction, Coinduction and Equality in Martin-Löf and Homotopy Type Theory

   Författare :Andrea Vezzosi; Chalmers tekniska högskola; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; NATURVETENSKAP; NATURAL SCIENCES; Conversion; Parametricity; Higher Inductive Types; Sized Types; Dependent Types; Type Theory; Guarded Types;

   Sammanfattning : Martin Löf Type Theory, having put computation at the center of logical reasoning, has been shown to be an effective foundation for proof assistants, with applications both in computer science and constructive mathematics. One ambition though is for MLTT to also double as a practical general purpose programming language. LÄS MER