swMATH34511MaRDI QIDQ46220FDOQ46220
Author name not available (Why is that?)
Official website: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.49.1311
Cited In (60)
- ANF preserves dependent types up to extensional equality
- Automated techniques for provably safe mobile code.
- 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
- AnZenMail
- Certifying low-level programs with hardware interrupts and preemptive threads
- BCEL
- Mnemonics
- DyC
- Flask
- BlenX
- SmallEiffel
- Formal enforcement of security policies on concurrent systems
- Time analysis of actor programs
- Java Jr
- Lincx
- JFlow
- ABS
- Kit
- Celf
- ASM
- TIL
- Fides
- Sancus
- Welterweight Java
- Piton
- A first-order one-pass CPS transformation
- A formal model of real-time program compilation
- On the relative expressiveness of higher-order session processes
- 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
- A representation of \(F_{\omega}\) in LF
- Flow analytic type system for array bound checks
- A list-machine benchmark for mechanized metatheory
- Verification of common interprocedural compiler optimizations using visibly pushdown Kleene algebra
- \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
