TALx86

swMATH34511MaRDI QIDQ46220

No author found.

Related Items (41)

Verified bytecode verification and type-certifying compilation ⋮ A first-order one-pass CPS transformation ⋮ Certifying low-level programs with hardware interrupts and preemptive threads ⋮ ANF preserves dependent types up to extensional equality ⋮ Polymorphic typed defunctionalization and concretization ⋮ Formal compiler construction in a logical framework ⋮ Towards imperative modules: reasoning about invariants and sharing of mutable state ⋮ A verifiable low-level concurrent programming model based on colored Petri nets ⋮ Certifying assembly programs with trails ⋮ Security types preserving compilation ⋮ A formally verified compiler back-end ⋮ An observationally complete program logic for imperative higher-order functions ⋮ Application of static analyses for state-space reduction to the microcontroller binary code ⋮ Time analysis of actor programs ⋮ A reduction semantics for direct-style asynchronous observables ⋮ A list-machine benchmark for mechanized metatheory ⋮ Function extraction ⋮ \textsc{Mnemonics}: type-safe bytecode generation at run time ⋮ Jaguar: enabling efficient communication and I/O in Java ⋮ A new type system for JVM lock primitives ⋮ Abstraction-carrying code: a model for mobile code safety ⋮ Fully abstract trace semantics for protected module architectures ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Stack-based typed assembly language ⋮ Type-based hot swapping of running modules ⋮ Types for the ambient calculus ⋮ On the relative expressiveness of higher-order session processes ⋮ Stack-based typed assembly language ⋮ Formal enforcement of security policies on concurrent systems ⋮ Verification of Common Interprocedural Compiler Optimizations Using Visibly Pushdown Kleene Algebra ⋮ On the Relative Expressiveness of Higher-Order Session Processes ⋮ A type system for the push-enter model ⋮ A note on complexity measures for inductive classes in constructive type theory ⋮ A Representation of Fω in LF ⋮ Observational program calculi and the correctness of translations ⋮ Automated techniques for provably safe mobile code. ⋮ safeDpi: a language for controlling mobile code ⋮ Type-Safe Code Transformations in Haskell ⋮ Lightweight Static Capabilities ⋮ A formal model of real-time program compilation

This page was built for software: TALx86