TALx86

swMATH34511MaRDI QIDQ46220FDOQ46220

Author name not available (Why is that?)

Cited In (41)

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

This page was built for software: TALx86