( en | de | ru )

 

  2. tag
  3. ocaml types

bookmarks  5

  •  

    Logically Qualified Data Types, abbreviated to Liquid Types, a system that combines Hindley-Milner type inference with Predicate Abstraction to automatically infer dependent types precise enough to prove a variety of safety properties. Liquid types allow programmers to reap many of the benefits of dependent types, namely static verification of critical properties and the elimination of expensive run-time checks, without manual annotation. We have implemented liquid type inference in Dsolve, which takes as input an Ocaml program and a set of logical qualifiers and infers dependent types for the expressions in the Ocaml program.We describe experiments using Dsolve to statically verify the safety of array accesses on a set of Ocaml benchmarks that were previously annotated as part of the DML project. When used with a simple set of bounds checking qualifiers, Dsolve reduces manual annotation required from 31% of program text to under 1%.
    13 years ago by @draganigajic
     
      csdependent-typesfpltuocamlpapertheorytypeTheorytypes
      (0)
      copydelete
       
       
    •  

      # Please note that Dependent ML (DML) is no longer under active development. As a language, it has already been fully incorporated into ATS. # Dependent ML (DML) is a conservative extension of the functional programming language ML. The type system of DML enriches that of ML with a restricted form of dependent types. This allows many interesting program properties such as memory safety and termination to be captured in the type system of DML and therefore be verified at compiler-time. # DML The current (undocumented) implementation of a DML type-checker can be found here, which is written in Objective Caml. The syntax of DML can be readily learned from the various examples included in the distribution given that one is already familiar with Standard ML. Also, termination checking is supported in this implementation. # de Caml is the Caml-light compiler extended with a front-end supporting DML style dependent types.
      13 years ago by @draganigajic
       
        csdependent-typesdmlmlocamlplprogrammingtypes
        (0)
        copydelete
         
         
      •  

        is an extension to MetaOCaml with indexed types. Indexed types allow the programmer to express nested polymorphism as well as complex functional dependencies at the level of types. Small number of extensions to the term and type language are needed to give the user full access to the powerful Coq proof checker at the level of types. With these extensions, datatypes can be defined that reflect the size of a list or a vector in its type. Because Coq is one of the most expressive checkers available, any fact that can be proved in Coq can be used to give more refined types to programs. Because Coq propositions can be viewed as types, Concoqtion provides a natural way to incorporate formal verification techniques into programming practice. * Related Systems: Epigram, Cayenne, ATS, Omega, Elf and Twelf, RSP, DML, Harper and Licata's extension to DML, Lightwight dependent types, Attractive types, First Class Phantom Types, GADTs for Object-oriented languages, Scala
        13 years ago by @draganigajic
         
          coqfpgadtmetaocamlocamltypes
          (0)
          copydelete
           
           
        •  

          G'Caml is a variant of O'Caml compiler which extends ML parametric polymorphism to non-parametric one, called extensional polymorphism. Freed from the clear but simple parametricity, G'Caml provides many useful features which were impossible or very hard to achieve in O'Caml, such as overloading, type safe value marshalling, ML value printer, etc., Overloading Values of different types can be overloaded to one identifier, i.e. (+) and (+.) will be unified! Built-in ML value printer Gprint.print prints your ML value as if you were in toplevel. You no longer need to define trivial but boring printers by yourself. Type safe value input/output Value marshaling (serialization) is now type-safe. Types of types are now checked at input, so that ill-typed value input is rejected at run-time, instead of crashing the program.
          13 years ago by @draganigajic
           
            genericmlocamltypes
            (0)
            copydelete
             
             
          •  

            13 years ago by @draganigajic
             
              ocamlpltypes
              (0)
              copydelete
               
               
            • ⟨⟨
            • ⟨
            • 1
            • ⟩
            • ⟩⟩

            publications  

              No matching posts.
            • ⟨⟨
            • ⟨
            • ⟩
            • ⟩⟩