Ott
From MaRDI portal
Software:13417
swMATH663MaRDI QIDQ13417FDOQ13417
Author name not available (Why is that?)
Cited In (31)
- Formalising and Verifying Reference Attribute Grammars in Coq
- Dynamic structural operational semantics
- Executable component-based semantics
- Safe zero-cost coercions for Haskell
- \texttt{slepice}: towards a verified implementation of type theory in type theory
- Mechanized metatheory revisited
- Binding operators for nominal sets
- Lem: A Lightweight Tool for Heavyweight Semantics
- 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
- Implementing type systems for the IDE with Xsemantics
- A Formalization of the C99 Standard in HOL, Isabelle and Coq
- On the effectiveness of higher-order logic programming in language-oriented programming
- Binders unbound
- Secure distributed programming with value-dependent types
- Secure distributed programming with value-dependent types
- Dualized Simple Type Theory
- A Rewriting Logic Approach to Type Inference
- αCheck: A mechanized metatheory model checker
- Encoding abstract syntax without fresh names
- BNF-style notation as it is actually used
- General Bindings and Alpha-Equivalence in Nominal Isabelle
- An ACL2 Tutorial
- Mechanized semantics for the clight subset of the C language
- Operational Reasoning for Concurrent Caml Programs and Weak Memory Models
- A trusted mechanised JavaScript specification
- Romeo: A system for more flexible binding-safe programming
- System description: lang-n-change -- a tool for transforming languages
- Term-generic logic
This page was built for software: Ott
