Sökning: "Victor Lopez Juan"

Hittade 2 avhandlingar innehållade orden Victor Lopez Juan.

1. 1. Practical Heterogeneous Unification for Dependent Type Checking

   Författare :Víctor López Juan; Chalmers tekniska högskola; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; unification; dependent types; type checking;

   Sammanfattning : Dependent types can specify in detail which inputs to a program are allowed, and how the properties of its output depend on the inputs. A program called the type checker assesses whether a program has a given type, thus detecting situations where the implementation of a program potentially differs from its intended behaviour. LÄS MER

3. 2. Practical Unification for Dependent Type Checking

   Författare :Víctor López Juan; Chalmers tekniska högskola; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; unification; type checking; dependent types; Functional Programming;

   Sammanfattning : When using popular dependently-typed languages such as Agda, Idris or Coq to write a proof or a program, some function arguments can be omitted, both to decrease code size and to improve readability.  Type checking such a program involves inferring a combination of these implicit arguments that makes the program type-correct. LÄS MER