swMATH663MaRDI QIDQ13417FDOQ13417
Author name not available (Why is that?)
Official website: http://www.cl.cam.ac.uk/~pes20/ott/
Cited In (75)
- Formalising and Verifying Reference Attribute Grammars in Coq
- Dynamic structural operational semantics
- Executable component-based semantics
- Safe zero-cost coercions for Haskell
- A trusted mechanised JavaSript specification
- \texttt{slepice}: towards a verified implementation of type theory in type theory
- Mechanized metatheory revisited
- Binding operators for nominal sets
- Program verification by coinduction
- A Brief Overview of HOL4
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- A formalized general theory of syntax with bindings: extended version
- Dualized simple type theory
- Implementing type systems for the IDE with Xsemantics
- On the effectiveness of higher-order logic programming in language-oriented programming
- HYBRID
- Jakarta
- Beluga
- JastAdd
- TinkerType
- Visual C#
- OCaml
- GHC
- MontiCore
- AURA
- Abella
- Bedwyr
- Lem
- K tool
- PLT Redex
- Gmeta
- LNgen
- PoplMark
- Nominal Isabelle
- RepLib
- TCB
- Spoofax
- FreshML
- K-Java
- SugarJ
- Delphin
- gradualizerDynamicSemantics
- Autosubst
- FreshOCaml
- HNT
- mini-ML
- Unbound
- Neverlang
- JavAdaptor
- Hackage
- Template-Coq
- ELPI
- K Prover
- MLsub
- Ruler
- Binders unbound
- Secure distributed programming with value-dependent types
- Secure distributed programming with value-dependent types
- A Rewriting Logic Approach to Type Inference
- αCheck: A mechanized metatheory model checker
- ADSafe
- GHCi
- Encoding abstract syntax without fresh names
- BNF-style notation as it is actually used
- General bindings and alpha-equivalence in Nominal Isabelle
- lang-n-play
- An ACL2 Tutorial
- Mechanized semantics for the clight subset of the C language
- Operational Reasoning for Concurrent Caml Programs and Weak Memory Models
- A formalization of the C99 standard in HOL, Isabelle and Coq
- Melange
- Lem: a lightweight tool for heavyweight semantics
- System description: lang-n-change -- a tool for transforming languages
- Term-generic logic
- Romeo: a system for more flexible binding-safe programming
This page was built for software: Ott
