TALx86
From MaRDI portal
Cited in
(64)- A type system for the push-enter model
- A note on complexity measures for inductive classes in constructive type theory
- StEAM
- SafeDpi
- JoCaml
- VLISP
- A formal model of real-time program compilation
- Fully abstract trace semantics for protected module architectures
- Type-based hot swapping of running modules
- AnZenMail
- Automated techniques for provably safe mobile code.
- Verified bytecode verification and type-certifying compilation
- A first-order one-pass CPS transformation
- A list-machine benchmark for mechanized metatheory
- Mnemonics
- BCEL
- Flask
- DyC
- On the relative expressiveness of higher-order session processes
- Formal enforcement of security policies on concurrent systems
- Observational program calculi and the correctness of translations
- Time analysis of actor programs
- A reduction semantics for direct-style asynchronous observables
- BlenX
- Types for the ambient calculus
- SmallEiffel
- safeDpi: a language for controlling mobile code
- A formally verified compiler back-end
- Jaguar: Enabling efficient communication and I/O in Java
- Stack-based typed assembly language
- On the relative expressiveness of higher-order session processes
- A representation of \(F_{\omega}\) in LF
- Flow analytic type system for array bound checks
- Type-safe code transformations in Haskell
- Lightweight static capabilities
- Verification of common interprocedural compiler optimizations using visibly pushdown Kleene algebra
- Java Jr
- Lincx
- JFlow
- ABS
- TIL
- Kit
- Celf
- ASM
- A verifiable low-level concurrent programming model based on colored Petri nets
- Certifying assembly programs with trails
- Sancus
- Fides
- Welterweight Java
- An observationally complete program logic for imperative higher-order functions
- Piton
- Function extraction
- Stack-based typed assembly language
- scientific article; zbMATH DE number 1746459 (Why is no real title available?)
- ANF preserves dependent types up to extensional equality
- Application of static analyses for state-space reduction to the microcontroller binary code
- \textsc{Mnemonics}: type-safe bytecode generation at run time
- Certifying low-level programs with hardware interrupts and preemptive threads
- Polymorphic typed defunctionalization and concretization
- Formal compiler construction in a logical framework
- Towards imperative modules: reasoning about invariants and sharing of mutable state
- Security types preserving compilation
- A new type system for JVM lock primitives
- Abstraction-carrying code: a model for mobile code safety
This page was built for software: TALx86