The following pages link to Xavier Leroy (Q848738):
Displaying 34 items.
- Compilation of extended recursion in call-by-value functional languages (Q848739) (← links)
- Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves (Q928671) (← links)
- Formal verification of a C-like memory model and its uses for verifying program transformations (Q945054) (← links)
- A verified framework for higher-order uncurrying optimizations (Q968367) (← links)
- Coinductive big-step operational semantics (Q1012129) (← links)
- Java bytecode verification: Algorithms and formalizations (Q1405988) (← links)
- A list-machine benchmark for mechanized metatheory (Q1945921) (← links)
- Verified compilation of floating-point computations (Q2352505) (← links)
- Mechanized semantics for the clight subset of the C language (Q2655325) (← links)
- A formally verified compiler back-end (Q2655327) (← links)
- (Q2871863) (← links)
- Validating LR(1) Parsers (Q2892741) (← links)
- A mechanized semantics for C++ object construction and destruction, with applications to resource management (Q2942898) (← links)
- A compiled implementation of strong reduction (Q2949209) (← links)
- Mechanized semantics (Q3060983) (← links)
- A syntactic theory of type generativity and sharing (Q3125226) (← links)
- Formal verification of translation validators (Q3189822) (← links)
- Mechanized Verification of CPS Transformations (Q3498467) (← links)
- (Q4417878) (← links)
- A modular module system (Q4507960) (← links)
- (Q4553258) (← links)
- (Q4738342) (← links)
- (Q4788555) (← links)
- Bytecode verification on Java smart cards (Q4791013) (← links)
- A Formally-Verified Alias Analysis (Q4916050) (← links)
- A simple, verified validator for software pipelining (Q5255064) (← links)
- Programming Languages and Systems (Q5308689) (← links)
- Formal certification of a compiler back-end or (Q5348912) (← links)
- Verified squared (Q5408525) (← links)
- Formal verification of object layout for c++ multiple inheritance (Q5408532) (← links)
- Program Logics for Certified Compilers (Q5494381) (← links)
- Types for Proofs and Programs (Q5898173) (← links)
- Programming Languages and Systems (Q5899008) (← links)
- Efficient extensional binary tries (Q6156636) (← links)
