HYBRID
Hybrid: a package for higher-order syntax in Isabelle and Coq.
Keywords for this software
References in zbMATH (referenced in 18 articles )
Showing results 1 to 18 of 18.
Sorted by year (- Gheri, Lorenzo; Popescu, Andrei: A formalized general theory of syntax with bindings: extended version (2020)
- Abel, Andreas; Allais, Guillaume; Hameer, Aliya; Pientka, Brigitte; Momigliano, Alberto; Schäfer, Steven; Stark, Kathrin: POPLMark reloaded: mechanizing proofs by logical relations (2019)
- Mahmoud, Mohamed Yousri; Felty, Amy P.: Formalization of metatheory of the quipper quantum programming language in a linear logic (2019)
- Miller, Dale: Mechanized metatheory Revisited (2019)
- Momigliano, Alberto; Pientka, Brigitte; Thibodeau, David: A case study in programming coinductive proofs: Howe’s method (2019)
- Cave, Andrew; Pientka, Brigitte: Mechanizing proofs with logical relations -- Kripke-style (2018)
- Felty, Amy; Momigliano, Alberto; Pientka, Brigitte: Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions (2018)
- Mahmoud, Mohamed Yousri; Felty, Amy P.: Formal meta-level analysis framework for quantum programming languages (2018)
- Xavier, Bruno; Olarte, Carlos; Reis, Giselle; Nigam, Vivek: Mechanizing focused linear logic in Coq (2018)
- Ferreira, Francisco; Pientka, Brigitte: Programs using syntax with first-class binders (2017)
- Kaiser, Jonas; Pientka, Brigitte; Smolka, Gert: Relating system F and (\lambda2): a case study in Coq, Abella and Beluga (2017)
- Crole, Roy L.; Furniss, Amy: Canonical HybridLF: extending Hybrid with dependent types (2016)
- Felty, Amy P.; Momigliano, Alberto; Pientka, Brigitte: The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey (2015)
- Popescu, Andrei; Roşu, Grigore: Term-generic logic (2015)
- Felty, Amy; Momigliano, Alberto: Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (2012)
- Gacek, Andrew; Miller, Dale; Nadathur, Gopalan: A two-level logic approach to reasoning about computations (2012)
- Tiu, Alwen; Momigliano, Alberto: Cut elimination for a logic with induction and co-induction (2012)
- Felty, Amy P.; Momigliano, Alberto: Hybrid: A definitional two-level approach to reasoning with higher-order abstract syntax (2008) ioport
Further publications can be found at: http://hybrid.di.unimi.it/publications.html