( en | de | ru )

 

  2. tag
  3. pl

bookmarks  214

  •  

    14 years ago by @joergh
     
      languagequeryturingplgrapg
      copydelete
       
       
    •  

      "OBJ" refers to the language family, with OBJ3, CafeOBJ, BOBJ. The OBJ are algebraic prog and spec languages, based on order sorted equational logic, possibly enriched with other logics (such as rewriting logic, hidden equational logic, or first order logic), with module system of parameterized programming They are logical languages, in the sense that their programs are sets of sentences in some logical system, and their operational semantics is given by deduction in that logical system. All recent OBJ languages use order sorted algebra, with a rigorous basis for user definable sub-types, multiple inheritance, overloading, multiple representations, coercions, etc. also user definable mixfix syntax, execution strategies, and memoization. All recent OBJ languages provide parameterized modules, module instantiation, views, module expressions, etc., to support very flexible program structuring and reuse The module systems of Ada, ML, C++ have all been influenced by the OBJ
      13 years ago by @draganigajic
       
        logicobj3plcsresearch
        copydelete
         
         
      •  

        K4 by EXAMPLE K4 is product of Kx Inc. http://kx.com 2006.02.23. 22:15 Attila Vrabecz (VrAbi) http://vrabi.web.elte.hu/k based on J by EXAMPLE by 06/11/2005 (C) Oleg Kobchenko http://olegykj.sourceforge.net
        13 years ago by @draganigajic
         
          codekplexample
          copydelete
           
           
        •  

          Advantages of Soft Typing This is a continuation of this discussion. The main points for soft typing are as follows. * Compile time type checks. Soft typing can catch the same amount of provable errors at compile time as static typing. * Automatic downcasts. Downcasts are done automatically assuming the program passes type checking. The main argument for explicit casts is that it provides the programmer with more information, but this is a misnomer. One does not have to write down information for it to be shown to him, so long as said information is inferrable. Note: whether or not you believe OCaml doesn't have casting is irrelevant, simply assume that, when I refer to casting, I also mean situations in which it's emulated. * Unimposing. Unless a piece of code is provably incorrect at compile time, the compiler can insert runtime checks.
          13 years ago by @draganigajic
           
            discussiontypingplltu
            copydelete
             
             
          •  

            1. What is a dependent type 1. ADT -- the simplest dependent-type 2. Singleton types 3. Branding: type proxies 2. Lightweight static capabilities 1. Abstract and Introduction 2. Formalization and proofs 3. Accompanying source code 3. The question of verification 4. Genuine Dependent-type systems This is a joint work with Chung-chieh Shan. We describe several approaches to lightweight dependent-type programming, letting us gain experience with dependent types on existing programming language systems All these lightweight approaches rely on type-level proxies for values, so we can statically express properties (e.g., equality, inequality) of the values that are not generally known until the run time. ``This much is clear: many programmers are already finding practical uses for the approximants to dependent types which mainstream functional languages (especially Haskell) admit, by hook or by crook.''
            13 years ago by @draganigajic
             
              typeshaskelldependent-typesolegKiselyovplmlcs
              copydelete
               
               

            publications  33