Now showing items 1-11 of 11

    • A Graphical Multistage Calculus 

      Ellner, Stephan; Taha, Walid (2005-07-22)
      While visual programming languages continue to gain popularity in domains ranging from scientific computing to real-time systems, the wealth of abstraction mechanisms, reasoning principles, and type systems developed over ...
    • C++.T Formalization in Isar 

      Siek, Jeremy G.; Taha, Walid (2005-12-16)
      A formal account of C++ templates, including the compile-time and run-time semantics. The main result is a proof of type safety. The proof is written in the Isar proof language and can be mechanically verified using the ...
    • Compiling dynamic languages via typed functional languages 

      Bandyopadhyay, Raj; Taha, Walid (2007-10-19)
      Dynamic languages enable rapid prototyping, while statically typed languages offer early error-detection and efficient execution. As a result, the usual practice in software development is to build a prototype in a dynamic ...
    • E-FRP With Priorities 

      Inoue, Jun; Kaiabachev, Roumen; Taha, Walid; Zhu, Angela (2009-07-15)
      E-FRP is declarative language for programming resource-bounded, event-driven systems. Its original high-level semantics requires that each event handler execute atomically. This facilitates reasoning about E-FRP programs, ...
    • Gradual Typing: Isabelle/Isar Formalization 

      Siek, Jeremy; Taha, Walid (2006-04-07)
      This report formalizes a gradual type system using the Isabelle/Isar proof language and proof assistant. Gradual typing combines static typing and dynamic typing in the same language, allowing a programmer to gradual migrate ...
    • Implicitly Heterogeneous Multi-stage Programming 

      Eckhardt, Jason; Kaiabachev, Roumen; Pašalić, Emir; Swadi, Kedar; Taha, Walid (2005-04-16)
      Previous work on semantics-based multi-stage programming (MSP) language design focused on homogeneous languages designs, where the generating and the generated languages are the same. Homogeneous designs simply add a ...
    • Mixing Indexed Types and Hindley-Milner Type Inference 

      Pašalić, Emir; Siek, Jeremy G.; Taha, Walid (2006-07-28)
      This paper addresses the question of how to extend OCaml’s Hindley-Milner type system with types indexed by logical propositions and proofs of the Coq theorem prover, thereby providing an expressive and extensible mechanism ...
    • Multi-stage Programming for Mainstream Languages 

      Abdelatif, Tamer; Inoue, Jun; Ricken, Mathias; Taha, Walid; Westbrook, Edwin; Yao, Yilong (2009-07-27)
      Multi-stage programming (MSP) provides a disciplined approach to run-time code generation. In the purely functional setting, it has been shown how MSP can be used to reduce the overhead of abstractions, allowing clean, ...
    • Reasoning About Multi-Stage Programs 

      Inoue, Jun; Taha, Walid (2011-10-15)
      We settle three basic questions that naturally arise when verifying multi-stage functional programs. Firstly, does adding staging to a language compromise any equalities that hold in the base language? Unfortunately it ...
    • Reasoning About Staged Programs 

      Inoue, Jun; Taha, Walid (2009-07-14)
      Multi-stage programming (MSP) is a style of writing program generators---programs which generate programs---supported by special annotations that direct construction, combination, and execution of object programs. Various ...
    • Static Type Inference for Specialization in a Telescoping Compiler 

      Allen, Eric; Kennedy, Ken; McCosh, Cheryl; Taha, Walid (2004-09-01)
      The telescoping languages approach achieves high performance from applications encoded as high-level scripts. The core idea is to pre-compile underlying libraries to generate multiple variants optimized for use indifferent ...