TALx86
From MaRDI portal
Software:46220
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