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 20 articles )

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

  1. Constable, Robert; Bickford, Mark: Intuitionistic completeness of first-order logic (2014)
  2. Palmgren, Erik; Wilander, Olov: Constructing categories and setoids of setoids in type theory (2014)
  3. James, Perry R.; Chalin, Patrice: Faster and more complete extended static checking for the Java modeling language (2010)
  4. Rioboo, Renaud: Invariants for the FoCaL language (2009)
  5. Amjad, Hasan: Data compression for proof replay (2008)
  6. Constable, Robert L.; Moczydlowski, Wojciech: Extracting programs from constructive HOL proofs via IZF set-theoretic semantics (2008)
  7. Hickey, Jason; Nogin, Aleksey; Yu, Xin; Kopylov, Alexei: Practical reflection for sequent logics (2007)
  8. Kang, Eunsuk; Aagaard, Mark D.: Improving the usability of HOL through controlled automation tactics (2007)
  9. Aboul-Hosn, Kamal; Kozen, Dexter: KAT-ML: an interactive theorem prover for Kleene algebra with tests (2006)
  10. Allen, S.F.; Bickford, M.; Constable, R.L.; Eaton, R.; Kreitz, C.; Lorigo, L.; Moran, E.: Innovations in computational type theory using Nuprl (2006)
  11. Hickey, Jason; Nogin, Aleksey: Formal compiler construction in a logical framework (2006)
  12. Hickey, Jason; Nogin, Aleksey; Yu, Xin; Kopylov, Alexei: Mechanized meta-reasoning using a hybrid HOAS/de Bruijn representation and reflection (2006)
  13. Nogin, Aleksey; Kopylov, Alexei: Formalizing type operations using the “image” type constructor (2006)
  14. Hickey, Jason; Nogin, Aleksey: Extensible hierarchical tactic construction in a logical framework (2004)
  15. Kreitz, Christoph: Building reliable, high-performance networks with the Nuprl proof development system (2004)
  16. Granicz, Adam; Zimmerman, Daniel M.; Hickey, Jason: Rewriting UNITY (2003)
  17. Hickey, Jason; Nogin, Aleksey; Constable, Robert L.; Aydemir, Brian E.; Barzilay, Eli; Bryukhov, Yegor; Eaton, Richard; Granicz, Adam; Kopylov, Alexei; Kreitz, Christoph; Krupski, Vladimir N.; Lorigo, Lori; Schmitt, Stephan; Witty, Carl; Yu, Xin: MetaPRL -- a modular logical environment (2003)
  18. Nogin, Aleksey; Hickey, Jason: Sequent schema for derived rules (2002)
  19. Kopylov, Alexei; Nogin, Aleksey: Markov’s principle for propositional type theory (2001)
  20. Hickey, Jason; Nogin, Aleksey: Fast tactic-based theorem proving (2000)