Cited in
(75)- Romeo: a system for more flexible binding-safe programming
- Formalising and Verifying Reference Attribute Grammars in Coq
- A formalized general theory of syntax with bindings: extended version
- General bindings and alpha-equivalence in Nominal Isabelle
- Executable component-based semantics
- On the effectiveness of higher-order logic programming in language-oriented programming
- A Brief Overview of HOL4
- Dynamic structural operational semantics
- \texttt{slepice}: towards a verified implementation of type theory in type theory
- A Rewriting Logic Approach to Type Inference
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- Lem: a lightweight tool for heavyweight semantics
- System description: lang-n-change -- a tool for transforming languages
- Safe zero-cost coercions for Haskell
- Implementing type systems for the IDE with Xsemantics
- A trusted mechanised JavaSript specification
- Binders unbound
- Secure distributed programming with value-dependent types
- HYBRID
- Secure distributed programming with value-dependent types
- 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
- Encoding abstract syntax without fresh names
- FreshML
- K-Java
- SugarJ
- Delphin
- gradualizerDynamicSemantics
- Autosubst
- FreshOCaml
- HNT
- mini-ML
- Unbound
- Neverlang
- JavAdaptor
- Hackage
- Template-Coq
- ELPI
- K Prover
- MLsub
- Ruler
- αCheck: A mechanized metatheory model checker
- Term-generic logic
- ADSafe
- GHCi
- Mechanized metatheory revisited
- Dualized simple type theory
- Binding operators for nominal sets
- lang-n-play
- Program verification by coinduction
- Operational Reasoning for Concurrent Caml Programs and Weak Memory Models
- An ACL2 Tutorial
- A formalization of the C99 standard in HOL, Isabelle and Coq
- Melange
- Mechanized semantics for the clight subset of the C language
- BNF-style notation as it is actually used
This page was built for software: Ott