Cited in
(64)- Automated techniques for provably safe mobile code.
- Abstraction-carrying code: a model for mobile code safety
- A formally verified compiler back-end
- Polymorphic typed defunctionalization and concretization
- A note on complexity measures for inductive classes in constructive type theory
- Types for the ambient calculus
- 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
- Stack-based typed assembly language
- Fully abstract trace semantics for protected module architectures
- An observationally complete program logic for imperative higher-order functions
- Function extraction
- Security types preserving compilation
- Lightweight static capabilities
- 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
- SafeDpi
- JoCaml
- StEAM
- VLISP
- AnZenMail
- BCEL
- Mnemonics
- DyC
- Flask
- BlenX
- SmallEiffel
- Java Jr
- Lincx
- JFlow
- ABS
- Kit
- Celf
- ASM
- TIL
- Fides
- Sancus
- Welterweight Java
- Piton
- Certifying low-level programs with hardware interrupts and preemptive threads
- Formal enforcement of security policies on concurrent systems
- Time analysis of actor programs
- A formal model of real-time program compilation
- A first-order one-pass CPS transformation
- On the relative expressiveness of higher-order session processes
- scientific article; zbMATH DE number 1746459 (Why is no real title available?)
- A verifiable low-level concurrent programming model based on colored Petri nets
- Certifying assembly programs with trails
- On the relative expressiveness of higher-order session processes
- 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
- \textsc{Mnemonics}: type-safe bytecode generation at run time
- Verification of common interprocedural compiler optimizations using visibly pushdown Kleene algebra
- 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
