Pages that link to "Item:Q2655327"
From MaRDI portal
The following pages link to A formally verified compiler back-end (Q2655327):
Displaying 30 items.
- Runtime verification of embedded real-time systems (Q479806) (← links)
- Impossibility of gathering, a certification (Q483063) (← links)
- Mechanising a type-safe model of multithreaded Java with a verified compiler (Q1663233) (← links)
- Verified spilling and translation validation with repair (Q1687761) (← links)
- A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data (Q1739908) (← links)
- Non-well-founded deduction for induction and coinduction (Q2055840) (← links)
- Safe functional systems through integrity types and verified assembly (Q2220814) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- A decision procedure for (co)datatypes in SMT solvers (Q2360873) (← links)
- Automatic refinement to efficient data structures: a comparison of two approaches (Q2417948) (← links)
- A resource semantics and abstract machine for \textit{Safe}: a functional language with regions and explicit deallocation (Q2437794) (← links)
- Proof-producing translation of higher-order logic into pure and stateful ML (Q2875232) (← links)
- Programming Inductive Proofs (Q3058448) (← links)
- Relational Decomposition (Q3087994) (← links)
- Animating the Formalised Semantics of a Java-Like Language (Q3088008) (← links)
- Coquet: A Coq Library for Verifying Hardware (Q3100217) (← links)
- Formal Certification of a Resource-Aware Language Implementation (Q3183530) (← links)
- Mining the Archive of Formal Proofs (Q3453102) (← links)
- A Decision Procedure for (Co)datatypes in SMT Solvers (Q3454092) (← links)
- Mechanized Verification of Computing Dominators for Formalizing Compilers (Q4916051) (← links)
- The verified CakeML compiler backend (Q4972072) (← links)
- Cogent: uniqueness types and certifying compilation (Q5019022) (← links)
- Trace-Relating Compiler Correctness and Secure Compilation (Q5041085) (← links)
- A Fast Verified Liveness Analysis in SSA Form (Q5049011) (← links)
- ANF preserves dependent types up to extensional equality (Q5051989) (← links)
- A Proof Score Approach to Formal Verification of an Imperative Programming Language Compiler (Q5056076) (← links)
- Trustworthy Graph Algorithms (Invited Talk) (Q5092359) (← links)
- Verifying Optimizations for Concurrent Programs (Q5240132) (← links)
- (Q5875439) (← links)
- Characteristic formulae for liveness properties of non-terminating CakeML programs (Q5875446) (← links)
