MetaPRL is two things: it is a logical framework where multiple logics can be defined and related, and it is a system implementation with support for interactive proof and automated reasoning. A primary feature of MetaPRL is a semantic connection to programming languages, that allows the system to be used as a logical programming environment, where programs are constructed as a mixture of specifications, implementations, and verifications.

References in zbMATH (referenced in 26 articles )

Showing results 1 to 20 of 26.
Sorted by year (citations)

1 2 next

  1. Carette, Jacques; Farmer, William M.; Laskowski, Patrick: HOL Light QE (2018)
  2. Farmer, William M.: Incorporating quotation and evaluation into Church’s type theory (2018)
  3. Rahli, Vincent; Bickford, Mark: Validating Brouwer’s continuity principle for numbers using named exceptions (2018)
  4. Fulton, Nathan; Mitsch, Stefan; Bohrer, Brandon; Platzer, André: Bellerophon: tactical theorem proving for hybrid systems (2017)
  5. Novak, Natalia: Practical extraction of evidence terms from common-knowledge reasoning (2015)
  6. Constable, Robert; Bickford, Mark: Intuitionistic completeness of first-order logic (2014)
  7. Palmgren, Erik; Wilander, Olov: Constructing categories and setoids of setoids in type theory (2014)
  8. de Moura, Leonardo; Passmore, Grant Olney: The strategy challenge in SMT solving (2013)
  9. James, Perry R.; Chalin, Patrice: Faster and more complete extended static checking for the Java modeling language (2010)
  10. Rioboo, Renaud: Invariants for the FoCaL language (2009)
  11. Amjad, Hasan: Data compression for proof replay (2008)
  12. Constable, Robert L.; Moczydlowski, Wojciech: Extracting programs from constructive HOL proofs via IZF set-theoretic semantics (2008)
  13. Hickey, Jason; Nogin, Aleksey; Yu, Xin; Kopylov, Alexei: Practical reflection for sequent logics (2007)
  14. Kang, Eunsuk; Aagaard, Mark D.: Improving the usability of HOL through controlled automation tactics (2007)
  15. Aboul-Hosn, Kamal; Kozen, Dexter: KAT-ML: an interactive theorem prover for Kleene algebra with tests (2006)
  16. Allen, S. F.; Bickford, M.; Constable, R. L.; Eaton, R.; Kreitz, C.; Lorigo, L.; Moran, E.: Innovations in computational type theory using Nuprl (2006)
  17. Hickey, Jason; Nogin, Aleksey: Formal compiler construction in a logical framework (2006)
  18. Hickey, Jason; Nogin, Aleksey; Yu, Xin; Kopylov, Alexei: Mechanized meta-reasoning using a hybrid HOAS/de Bruijn representation and reflection (2006)
  19. Nogin, Aleksey; Kopylov, Alexei: Formalizing type operations using the “image” type constructor (2006)
  20. Hickey, Jason; Nogin, Aleksey: Extensible hierarchical tactic construction in a logical framework (2004)

1 2 next