• KLAIM

  • Referenced in 71 articles [sw09424]
  • KLAIM is equipped with a type system that statically checks access right violations of mobile...
  • PROGRES

  • Referenced in 70 articles [sw02905]
  • systems. An integrated type-checker is able to check the static semantics of a specification...
  • ALDOR

  • Referenced in 27 articles [sw01220]
  • programs. Pervasive support for dependent types allows static checking of dynamic objects. What does this...
  • TCOZ

  • Referenced in 8 articles [sw03382]
  • based static type checking and dynamic visualization for TCOZ Timed Communicating Object Z (TCOZ) combines ... demonstrates the development of a type checker for detecting static semantic errors of the TCOZ...
  • CCured

  • Referenced in 24 articles [sw10057]
  • time checking to make existing C programs type safe. We describe the CCured type system ... separating pointer types according to their usage. This type system allows both pointers whose usage ... verified statically to be type safe, and pointers whose safety must be checked ... pointers are statically verifiable to be type safe. The remaining pointers are instrumented with efficient...
  • Sage

  • Referenced in 4 articles [sw30073]
  • refinement types. Since type checking for this expressive language is not statically decidable, Sage ... uses hybrid type checking, which extends static type checking with dynamic contract checking, automatic theorem...
  • Fortress

  • Referenced in 16 articles [sw13026]
  • intended to provide static checking of an expressive type system, implicit, abundant parallelism managing with...
  • Sather

  • Referenced in 8 articles [sw34049]
  • oriented language with garbage collection, statically-checked strong typing, multiple inheritance, separate implementations and type...
  • JFlow

  • Referenced in 26 articles [sw20595]
  • label model, label polymorphism, run-time label checking, and automatic label inference. JFlow also supports ... integrated successfully with static information flow control, including objects, subclassing, dynamic type tests, access control ... used to check JFlow programs for correctness. Because most checking is static, there is little...
  • ETCH

  • Referenced in 3 articles [sw07636]
  • performs only limited type checking. In particular, SPIN does not guarantee static detection of mismatched ... types of channels are only partially specified in Promela. ETCH extends the type checking capabilities ... missing channel type information, allowing strong static type checking. Thus ETCH can detect type errors...
  • XDuce

  • Referenced in 54 articles [sw12436]
  • processing language. XDuce is a statically typed programming language for XML processing. Its basic data ... documents, and its types (so-called regular expression types) directly correspond to document schemas. XDuce ... expression pattern matching, integrating conditional branching, tag checking, and subtree extraction, as well as dynamic...
  • Metaphor

  • Referenced in 2 articles [sw08956]
  • multi-stage and provides static type checking of later stage code. Object-oriented frameworks usually...
  • CLEAN

  • Referenced in 58 articles [sw01346]
  • with both static as well as dynamic typing. Expressions, which are dynamically typed, are called ... make plug-ins which will be type checked at run-time. Typically...
  • CiaoPP

  • Referenced in 44 articles [sw12089]
  • predicates and literals of the program, including types, modes and other variable instantiation properties ... static debugging and verification, finding errors before running the program. This includes checking how programs...
  • ScalaQL

  • Referenced in 3 articles [sw13850]
  • that is statically checked and type safe. Unfortunately, certain language changes or core design elements...
  • PolyTOIL

  • Referenced in 23 articles [sw14205]
  • statically-typed polymorphic object-oriented programming language which is provably type-safe. By separating ... name for the type of self, and carefully defining the type-checking rules, we have...
  • Error Prone

  • Referenced in 1 article [sw28472]
  • doesn’t do much beyond static type checking. Using Error Prone to augment the compiler...
  • BoogiePL

  • Referenced in 13 articles [sw21521]
  • BoogiePL: A typed procedural language for checking object-oriented programs. This note defines BoogiePL ... verification. The language is a simple coarsely typed imperative language with procedures and arrays, plus ... accepted as input to Boogie, the Spec# static program verifier...
  • SAFECode

  • Referenced in 4 articles [sw13323]
  • Weakly Typed Languages. Static analysis of programs in weakly typed languages such ... less precise ones), a call graph, and type information for a subset of memory ... type system with the necessary run-time checks in operational semantics and prove the correctness ... semantics provide the foundation for other sophisticated static analyses to be applied to C programs...
  • HLIO

  • Referenced in 3 articles [sw22611]
  • typically enforced via type systems and static analyses or via dynamic execution monitors ... give programmers the flexibility of deferring IFC checks to runtime (as in LIO), while also ... parts of their programs that can be statically verified (unlike LIO). We present the design ... novel technique for deferring IFC checks based on singleton types and constraint polymorphism. We formalize...