• ML

  • Referenced in 517 articles [sw01218]
  • requiring explicit type annotations, and ensures type safety – there is a formal proof that...
  • Twelf

  • Referenced in 169 articles [sw06888]
  • proof-carrying-code system, and a type safety proof for Standard...
  • Featherweight Java

  • Referenced in 91 articles [sw16204]
  • arguments about key properties such as type safety. We carry this process a step further ... following Java’s. A proof of type safety for Featherweight Java thus illustrates many ... safety proof for the full language, while remaining pleasingly compact. The minimal syntax, typing rules ... give a detailed proof of type safety. The extended system formalizes for the first time...
  • XDuce

  • Referenced in 54 articles [sw12436]
  • core, along with a proof of type safety...
  • CIL

  • Referenced in 36 articles [sw26691]
  • with run-time checks to ensure type safety. CIL has served us very well...
  • PolyTOIL

  • Referenced in 23 articles [sw14205]
  • rules and semantics. A proof of type safety is obtained with...
  • Dylan

  • Referenced in 13 articles [sw26095]
  • systems programming. Dylan includes garbage collection, type-safety, error recovery, a module system, and programmer...
  • PLAN

  • Referenced in 13 articles [sw22065]
  • guarantees to the programmer, such as type safety. A more novel property aimed at protecting...
  • MJ

  • Referenced in 12 articles [sw24342]
  • give a proof of type safety. In order to demonstrate the usefulness...
  • CCured

  • Referenced in 24 articles [sw10057]
  • verified statically to be type safe, and pointers whose safety must be checked...
  • Jinja Threads

  • Referenced in 9 articles [sw28538]
  • source and byte code and show type safety for the multithreaded case. Equally, the compiler...
  • PolyAML

  • Referenced in 4 articles [sw08950]
  • representative for all of its children. Type safety requires that the type of each child...
  • TS#

  • Referenced in 3 articles [sw14208]
  • with various checks to ensure the type safety of TS# despite its interactions with arbitrary ... main theorem employs a form of type-preserving compilation, wherein we prove all the runtime ... typed in JS# , a previously proposed dependently typed language for proving functional correctness of JavaScript ... JavaScript, while providing strong safety guarantees by virtue of typing...
  • HMC

  • Referenced in 7 articles [sw09867]
  • algorithm that reduces verification of safety properties of typed higher-order functional programs to interprocedural ... works as follows. First, it uses the type structure of the functional program to generate ... logical refinement constraints whose satisfaction implies the safety of the source program. Next, it transforms ... interproc – to verify ocaml programs. By composing type-based reasoning grounded in program syntax...
  • COUPLEX

  • Referenced in 31 articles [sw07861]
  • safety assessments in nuclear waste management. It leads to a classical convection diffusion type problem...
  • Jinja not Java

  • Referenced in 2 articles [sw28876]
  • definite initialisation analysis; a type safety proof of the small step semantics; a virtual machine ... semantics and its type system; a type safety proof for the JVM; a bytecode verifier ... proof of the bytecode verifier w.r.t. the type system; a compiler and a proof that...
  • SIGNAL

  • Referenced in 51 articles [sw02915]
  • however made a difficult issue by global safety requirements. To enable separate compilation ... module system for SIGNAL. Just as data-types describe the invariants of program modules...
  • XPi

  • Referenced in 7 articles [sw09430]
  • static and dynamic typing. In XPi, a type system disciplines XML message handling ... processes. A run-time safety theorem ensures that in well-typed systems no service will...
  • NL2Type

  • Referenced in 1 article [sw31110]
  • dynamically typed and hence lacks the type safety of statically typed languages, leading to suboptimal...
  • SPY

  • Referenced in 6 articles [sw22152]
  • theory of multiparty session types, our toolchain implementation validates communication safety properties on the global ... occurrence of illegal communication actions and message types that do not conform to the protocol...