This site uses cookies to deliver our services and to ensure you get the best experience. By continuing to use this site, you consent to our use of cookies and acknowledge that you have read and understand our Privacy Policy, Cookie Policy, and Terms
Most current techniques fail to achieve the dynamic update of recursive functions. A focus on execution states appears to be essential in order to implement dynamic update in this...
While many type systems based on the intuitionistic fragment of linear logic have been proposed, applications in programming languages of the full power of linear logic--including...
We describe the design, implementation, and use of a machinecertified framework for correct compilation and execution of programs in garbage-collected languages. Our framework ext...
Andrew McCreight, Tim Chevalier, Andrew P. Tolmach
We present a technique for higher-order representation of substructural logics such as linear or modal logic. We show that such logics can be encoded in the (ordinary) Logical Fra...
Modern proof assistants such as Coq and Isabelle provide high degrees of expressiveness and assurance because they support formal reasoning in higher-order logic and supply explic...
Several recent security-typed programming languages, such as Aura, PCML5, and Fine, allow programmers to express and enforce access control and information flow policies. Most of ...
A wide range of computer programs, including compilers and theorem provers, manipulate data structures that involve names and binding. However, the design of programming idioms wh...
We present a case-study of using OCaml within a large product development project, focussing on both the technical and nontechnical issues that arose as a result. We draw comparis...
David Scott, Richard Sharp, Thomas Gazagnaire, Ani...