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

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

1 2 next

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

1 2 next