Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
71 | Christian Urban, James Cheney, Stefan Berghofer |
Mechanizing the Metatheory of LF. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LICS ![In: Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA, pp. 45-56, 2008, IEEE Computer Society, 978-0-7695-3183-0. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
mechanized metatheory, logical frameworks, nominal logic |
57 | Benjamin C. Pierce, Peter Sewell, Stephanie Weirich, Steve Zdancewic |
It Is Time to Mechanize Programming Language Metatheory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
VSTTE ![In: Verified Software: Theories, Tools, Experiments, First IFIP TC 2/WG 2.3 Conference, VSTTE 2005, Zurich, Switzerland, October 10-13, 2005, Revised Selected Papers and Discussions, pp. 26-30, 2005, Springer, 978-3-540-69147-1. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
57 | Robin Adams 0001 |
Formalized Metatheory with Terms Represented by an Indexed Family of Types. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers, pp. 1-16, 2004, Springer, 3-540-31428-8. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
57 | Douglas J. Howe |
Computational Metatheory in Nuprl. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 9th International Conference on Automated Deduction, Argonne, Illinois, USA, May 23-26, 1988, Proceedings, pp. 238-257, 1988, Springer, 3-540-19343-X. The full citation details ...](Pics/full.jpeg) |
1988 |
DBLP DOI BibTeX RDF |
formal metamathematics, reflection, Theorem proving, type theory, constructive mathematics, tactics |
54 | Daniel K. Lee, Karl Crary, Robert Harper 0001 |
Towards a mechanized metatheory of standard ML. ![Search on Bibsonomy](Pics/bibsonomy.png) |
POPL ![In: Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007, pp. 173-184, 2007, ACM, 1-59593-575-4. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
language definitions, mechanized metatheory, twelf, standard ML, logical frameworks, type safety |
40 | Brian E. Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, Stephanie Weirich |
Engineering formal metatheory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
POPL ![In: Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, pp. 3-15, 2008, ACM, 978-1-59593-689-9. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
locally nameless, binding, coq |
40 | Andreas Abel 0001, Dulma Rodriguez |
Syntactic Metatheory of Higher-Order Subtyping. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CSL ![In: Computer Science Logic, 22nd International Workshop, CSL 2008, 17th Annual Conference of the EACSL, Bertinoro, Italy, September 16-19, 2008. Proceedings, pp. 446-460, 2008, Springer, 978-3-540-87530-7. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
Higher-order subtyping, bounded quantification, algorithmic subtyping, hereditary substitution |
40 | James Cheney, Alberto Momigliano |
Mechanized metatheory model-checking. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PPDP ![In: Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 14-16, 2007, Wroclaw, Poland, pp. 75-86, 2007, ACM, 978-1-59593-769-8. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
counterexample search, model checking, nominal logic |
40 | Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, Steve Zdancewic |
Mechanized Metatheory for the Masses: The PoplMark Challenge. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings, pp. 50-65, 2005, Springer, 3-540-28372-2. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
40 | Fiora Pirri, Raymond Reiter |
Some Contributions to the Metatheory of the Situation Calculus. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. ACM ![In: J. ACM 46(3), pp. 325-361, 1999. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
programming languages for the situation calculus, theorem-proving, regression, situation calculus |
40 | Amy P. Felty, Douglas J. Howe, Abhik Roychoudhury |
Formal Metatheory using Implicit Syntax, and an Application to Data Abstraction for Asynchronous Systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings, pp. 237-251, 1999, Springer, 3-540-66222-7. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
40 | David A. Basin, Seán Matthews |
Structuring Metatheory on Inductive Definitions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30 - August 3, 1996, Proceedings, pp. 171-185, 1996, Springer, 3-540-61511-3. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
34 | Manuel Clavel, Francisco Durán 0001, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer 0001, Carolyn L. Talcott |
Reflection, Metalevel Computation, and Strategies. ![Search on Bibsonomy](Pics/bibsonomy.png) |
All About Maude ![In: All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, pp. 419-458, 2007, Springer, 978-3-540-71940-3. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
34 | Seán Matthews |
A Practical Implementation of Simple Consequence Relations Using Inductive Definitions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-14, 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13-17, 1997, Proceedings, pp. 306-320, 1997, Springer, 3-540-63104-6. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
31 | Ralph L. London |
Certification of algorithm 245 [M1]: treesort 3: proof of algorithms - a new kind of certification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Commun. ACM ![In: Commun. ACM 13(6), pp. 371-373, 1970. The full citation details ...](Pics/full.jpeg) |
1970 |
DBLP DOI BibTeX RDF |
in-place sorting, metatheory, proof of algorithms, debugging, sorting, certification |
23 | Mario Carneiro |
Lean4Lean: Towards a formalized metatheory for the Lean theorem prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2403.14064, 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP DOI BibTeX RDF |
|
23 | Ende Jin, Nada Amin, Yizhou Zhang 0001 |
Extensible Metatheory Mechanization via Family Polymorphism. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proc. ACM Program. Lang. ![In: Proc. ACM Program. Lang. 7(PLDI), pp. 1608-1632, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
23 | Michalis Kokologiannakis, Ori Lahav 0001, Viktor Vafeiadis |
Kater: Automating Weak Memory Model Metatheory and Consistency Checking. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proc. ACM Program. Lang. ![In: Proc. ACM Program. Lang. 7(POPL), pp. 544-572, January 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
23 | Takahiro Yamada |
Wright's Strict Finitistic Logic in the Classical Metatheory: The Propositional Case. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Philos. Log. ![In: J. Philos. Log. 52(4), pp. 1081-1100, August 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
23 | Maristela Rocha |
A Study of the Metatheory of Assertoric Syllogistic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Logica Universalis ![In: Logica Universalis 17(3), pp. 347-371, September 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
23 | Rafaël Bocquet, Ambrus Kaposi, Christian Sattler |
For the Metatheory of Type Theory, Internal Sconing Is Enough. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2302.05190, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
23 | Javier Díaz |
Metatheory of Q0. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2023, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP BibTeX RDF |
|
23 | Rafaël Bocquet, Ambrus Kaposi, Christian Sattler |
For the Metatheory of Type Theory, Internal Sconing Is Enough. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FSCD ![In: 8th International Conference on Formal Structures for Computation and Deduction, FSCD 2023, July 3-6, 2023, Rome, Italy, pp. 18:1-18:23, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-277-8. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
23 | Jeremy G. Siek |
The Metatheory of Gradual Typing: State of the Art and Challenges (Invited Talk). ![Search on Bibsonomy](Pics/bibsonomy.png) |
CALCO ![In: 10th Conference on Algebra and Coalgebra in Computer Science, CALCO 2023, June 19-21, 2023, Indiana University Bloomington, IN, USA, pp. 4:1-4:1, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-287-7. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
23 | Marcelo Fiore, Dmitrij Szamozvancev |
Formal metatheory of second-order abstract syntax. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proc. ACM Program. Lang. ![In: Proc. ACM Program. Lang. 6(POPL), pp. 1-29, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
23 | Guillermo Badia, Zach Weber, Patrick Girard 0004 |
Paraconsistent Metatheory: New Proofs with Old Tools. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Philos. Log. ![In: J. Philos. Log. 51(4), pp. 825-856, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
23 | Frederik Krogsdal Jacobsen, Jørgen Villadsen |
Teaching Functional Programmers Logic and Metatheory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TFPIE ![In: Proceedings Tenth and Eleventh International Workshop on Trends in Functional Programming In Education, TFPIE 2021 / 2022, Kraków, Poland (online), 16th February 2021 / 16th March 2022., pp. 74-92, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
23 | Marcelo Fiore, Dmitrij Szamozvancev |
Formal Metatheory of Second-Order Abstract Syntax. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2201.03504, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP BibTeX RDF |
|
23 | Jonathan Sterling |
First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2022 |
DOI RDF |
|
23 | Ernesto Copello, Nora Szasz, Álvaro Tasistro |
Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Math. Struct. Comput. Sci. ![In: Math. Struct. Comput. Sci. 31(3), pp. 341-360, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
23 | Amy P. Felty, Carlos Olarte, Bruno Xavier |
A focused linear logical framework and its application to metatheory of object logics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Math. Struct. Comput. Sci. ![In: Math. Struct. Comput. Sci. 31(3), pp. 312-340, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
23 | Andrew Joseph McCarthy |
Modal Metatheory for Quantified Modal Logic, With and Without the Barcan Formulas. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Notre Dame J. Formal Log. ![In: Notre Dame J. Formal Log. 62(2), 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
23 | Alessandro Cheli |
Metatheory.jl: Fast and Elegant Algebraic Computation in Julia with Extensible Equality Saturation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Open Source Softw. ![In: J. Open Source Softw. 6(59), pp. 3078, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
23 | Fabrizio Montesi, Marco Peressotti |
Linear Logic, the π-calculus, and their Metatheory: A Recipe for Proofs as Processes. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2106.11818, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
23 | Alessandro Cheli |
Metatheory.jl: Fast and Elegant Algebraic Computation in Julia with Extensible Equality Saturation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2102.07888, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
23 | Jacob Errington, Junyoung Jang 0001, Brigitte Pientka |
Harpoon: Mechanizing Metatheory Interactively - (System Description). ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, pp. 636-648, 2021, Springer, 978-3-030-79875-8. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
23 | David Castro-Perez, Francisco Ferreira 0001, Lorenzo Gheri, Nobuko Yoshida |
Zooid: a DSL for certified multiparty computation: from mechanised metatheory to certified multiparty processes. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PLDI ![In: PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021., pp. 237-251, 2021, ACM, 978-1-4503-8391-2. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
23 | James Wood, Robert Atkey |
A Linear Algebra Approach to Linear Metatheory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Linearity&TLLA@IJCAR-FSCD ![In: Proceedings Second Joint International Workshop on Linearity & Trends in Linear Logic and Applications, Linearity&TLLA@IJCAR-FSCD 2020, Online, 29-30 June 2020., pp. 195-212, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
23 | Patrick Girard 0004, Zach Weber |
Modal Logic without Contraction in a Metatheory without Contraction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Rev. Symb. Log. ![In: Rev. Symb. Log. 12(4), pp. 685-701, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
23 | Dale Miller 0001 |
Mechanized Metatheory Revisited. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 63(3), pp. 625-665, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
23 | Mohamed Yousri Mahmoud, Amy P. Felty |
Formalization of Metatheory of the Quipper Quantum Programming Language in a Linear Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 63(4), pp. 967-1002, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
23 | Jasmin Christian Blanchette |
Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk). ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, pp. 1-13, 2019, ACM, 978-1-4503-6222-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
23 | Megan Katsumi, Michael Grüninger |
The metatheory of ontology reuse. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Appl. Ontology ![In: Appl. Ontology 13(3), pp. 225-254, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
23 | James E. Cutting, Kacie L. Armstrong |
Cryptic Emotions and the Emergence of a Metatheory of Mind in Popular Filmmaking. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Cogn. Sci. ![In: Cogn. Sci. 42(4), pp. 1317-1344, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
23 | Mohamed Yousri Mahmoud, Amy P. Felty |
Formalization of Metatheory of the Quipper Quantum Programming Language in a Linear Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1812.03624, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
23 | Georg Schiemer, Richard Zach, Erich H. Reck |
Carnap's early metatheory: scope and limits. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Synth. ![In: Synth. 194(1), pp. 33-65, 2017. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
23 | Ernesto Copello, Nora Szasz, Alvaro Tasistro |
Formal metatheory of the Lambda calculus using Stoughton's substitution. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Theor. Comput. Sci. ![In: Theor. Comput. Sci. 685, pp. 65-82, 2017. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
23 | James Cheney, Alberto Momigliano |
αCheck: A mechanized metatheory model-checker. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1704.00617, 2017. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP BibTeX RDF |
|
23 | Michael Rawson |
Verified Metatheory and Type Inference for a Name-Carrying Simply-Typed Lambda Calculus. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2017, 2017. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP BibTeX RDF |
|
23 | James Cheney, Alberto Momigliano |
αCheck: A mechanized metatheory model checker. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Theory Pract. Log. Program. ![In: Theory Pract. Log. Program. 17(3), pp. 311-352, 2017. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
23 | Dale Miller 0001 |
Mechanized Metatheory Revisited: An Extended Abstract (Invited Paper). ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia, pp. 1:1-1:16, 2016, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-065-1. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP DOI BibTeX RDF |
|
23 | David Darais, David Van Horn |
Constructive Galois connections: taming the Galois connection framework for mechanized metatheory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFP ![In: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016, pp. 311-324, 2016, ACM, 978-1-4503-4219-3. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP DOI BibTeX RDF |
|
23 | Christian Doczkal |
A machine-checked constructive metatheory of computation tree logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2016 |
RDF |
|
23 | Omar Alaqeeli |
The metatheory of the monadic hybrid calculus. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2016 |
RDF |
|
23 | Albert Meijer 0001, Victor Bekkers |
A metatheory of e-government: Creating some order in a fragmented research field. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Gov. Inf. Q. ![In: Gov. Inf. Q. 32(3), pp. 237-245, 2015. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
23 | David Darais, David Van Horn |
Constructive Galois Connections: Taming the Galois Connection Framework for Mechanized Metatheory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1511.06965, 2015. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP BibTeX RDF |
|
23 | David Darais, Matthew Might, David Van Horn |
Galois transformers and modular abstract interpreters: reusable metatheory for program analysis. ![Search on Bibsonomy](Pics/bibsonomy.png) |
OOPSLA ![In: Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, part of SPLASH 2015, Pittsburgh, PA, USA, October 25-30, 2015, pp. 552-571, 2015, ACM, 978-1-4503-3689-5. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
23 | Kaustuv Chaudhuri, Matteo Cimini, Dale Miller 0001 |
A Lightweight Formalization of the Metatheory of Bisimulation-Up-To. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pp. 157-166, 2015, ACM, 978-1-4503-3296-5. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
23 | Peter Johan Lor |
Revitalizing comparative library and information science: theory and metatheory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Documentation ![In: J. Documentation 70(1), pp. 25-51, 2014. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
23 | Leon James, Diane Nahl |
A metatheory integrating social, biological and technological factors in information behavior research. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Webology ![In: Webology 11(1), 2014. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP BibTeX RDF |
|
23 | Jonghyun Park, Jeongbong Seo, Sungwoo Park, Gyesik Lee |
Mechanizing Metatheory Without Typing Contexts. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 52(2), pp. 215-239, 2014. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
23 | Rodrigo Geraldo Ribeiro, Lucília Figueiredo, Carlos Camarão 0001 |
Mechanized metatheory for a λ-calculus with trust types. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Braz. Comput. Soc. ![In: J. Braz. Comput. Soc. 19(4), pp. 433-443, 2013. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
23 | Andrew Bacon |
Non-classical Metatheory for Non-classical Logics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Philos. Log. ![In: J. Philos. Log. 42(2), pp. 335-355, 2013. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
23 | Andreas Schropp, Andrei Popescu 0001 |
Nonfree Datatypes in Isabelle/HOL - Animating a Many-Sorted Metatheory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Certified Programs and Proofs - Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings, pp. 114-130, 2013, Springer, 978-3-319-03544-4. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
23 | Jasmin Christian Blanchette, Andrei Popescu 0001 |
Mechanizing the Metatheory of Sledgehammer. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FroCos ![In: Frontiers of Combining Systems - 9th International Symposium, FroCoS 2013, Nancy, France, September 18-20, 2013. Proceedings, pp. 245-260, 2013, Springer, 978-3-642-40884-7. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
23 | Kim G. Larsen, Radu Mardare, Claus R. Thrane |
Parameterized Metatheory for Continuous Markovian Logic ![Search on Bibsonomy](Pics/bibsonomy.png) |
QFM ![In: Proceedings Quantities in Formal Methods, QFM 2012, Paris, France, 28 August 2012., pp. 33-47, 2012. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
23 | Radu Mardare, Luca Cardelli, Kim G. Larsen |
Continuous Markovian Logics - Axiomatization and Quantified Metatheory ![Search on Bibsonomy](Pics/bibsonomy.png) |
Log. Methods Comput. Sci. ![In: Log. Methods Comput. Sci. 8(4), 2012. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
23 | Andrew W. Appel, Robert Dockins, Xavier Leroy |
A List-Machine Benchmark for Mechanized Metatheory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 49(3), pp. 453-491, 2012. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
23 | Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi |
Formal Metatheory of Programming Languages in the Matita Interactive Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 49(3), pp. 427-451, 2012. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
23 | Gyesik Lee, Bruno C. d. S. Oliveira, Sungkeun Cho, Kwangkeun Yi |
GMeta: A Generic Formal Metatheory Framework for First-Order Representations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ESOP ![In: Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings, pp. 436-455, 2012, Springer, 978-3-642-28868-5. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
23 | Victor Raskin |
A Little Metatheory: Thought on What aTheory of Computational Humor Should Look Like. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AAAI Fall Symposium: Artificial Intelligence of Humor ![In: Artificial Intelligence of Humor, Papers from the 2012 AAAI Fall Symposium, Arlington, Virginia, USA, November 2-4, 2012, 2012, AAAI. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP BibTeX RDF |
|
23 | Christian Urban, James Cheney, Stefan Berghofer |
Mechanizing the metatheory of LF. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Trans. Comput. Log. ![In: ACM Trans. Comput. Log. 12(2), pp. 15:1-15:42, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
23 | Robert E. Kent |
The Information Flow Framework: A Descriptive Category Metatheory ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1108.4133, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP BibTeX RDF |
|
23 | James Cheney, Christian Urban |
Mechanizing the Metatheory of mini-XQuery. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings, pp. 280-295, 2011, Springer, 978-3-642-25378-2. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
23 | Wilmer Ricciotti |
Theoretical and implementation aspects in the mechanization of the metatheory of programming languages. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2011 |
RDF |
|
23 | Patricia Johann, Alex Simpson, Janis Voigtländer |
A Generic Operational Metatheory for Algebraic Effects. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LICS ![In: Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, 11-14 July 2010, Edinburgh, United Kingdom, pp. 209-218, 2010, IEEE Computer Society, 978-0-7695-4114-3. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
23 | Christian Urban, James Cheney, Stefan Berghofer |
Mechanizing the Metatheory of LF ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/0804.1667, 2008. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP BibTeX RDF |
|
23 | Andreas Herzig, Ivan José Varzinczak |
Metatheory of actions: Beyond consistency. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Artif. Intell. ![In: Artif. Intell. 171(16-17), pp. 951-984, 2007. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
23 | Robert Harper 0001, Daniel R. Licata |
Mechanizing metatheory in a logical framework. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Funct. Program. ![In: J. Funct. Program. 17(4-5), pp. 613-673, 2007. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
23 | Andrew W. Appel, Xavier Leroy |
A List-machine Benchmark for Mechanized Metatheory: (Extended Abstract). ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP@FLoC ![In: Proceedings of the First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FLoC 2006, Seattle, WA, USA, August 16, 2006, pp. 95-108, 2006, Elsevier. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
23 | Andreas Herzig, Ivan José Varzinczak |
Metatheory of actions: beyond consistency ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/cs/0603034, 2006. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP BibTeX RDF |
|
23 | Miroljub Dugic, Milan M. Cirkovic, Dejan Rakovic |
On a Possible Physical Metatheory of Consciousness. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Open Syst. Inf. Dyn. ![In: Open Syst. Inf. Dyn. 9(2), pp. 153-166, 2002. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
23 | Joseph Vanderwaart, Karl Crary |
A Simplified Account of the Metatheory of Linear LF. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFM ![In: International Workshop on Logical Frameworks and Meta-Languages, LFM 2002, FLoC Satellite Event, Copenhagen, Denmark, July 26, 2002, pp. 11-28, 2002, Elsevier. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
23 | David A. Basin, Seán Matthews |
Structuring Metatheory on Inductive Definitions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Inf. Comput. ![In: Inf. Comput. 162(1-2), pp. 80-95, 2000. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
23 | Brenda Dervin |
On studying information seeking methodologically: the implications of connecting metatheory to method. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Inf. Process. Manag. ![In: Inf. Process. Manag. 35(6), pp. 727-750, 1999. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
23 | Erik Sandewall |
Cognitive Robotics Logic and its Metatheory: Features and Fluents Revisited. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Electron. Trans. Artif. Intell. ![In: Electron. Trans. Artif. Intell. 2, pp. 307-329, 1998. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP BibTeX RDF |
|
23 | Alessandro Armando, Jason Gallagher, Alan Smaill, Alan Bundy |
Automating the Synthesis of Decision Procedures in a Constructive Metatheory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Ann. Math. Artif. Intell. ![In: Ann. Math. Artif. Intell. 22(3-4), pp. 259-279, 1998. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
23 | Birger Hjørland |
Theory and metatheory of information science: a new interpretation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Documentation ![In: J. Documentation 54(5), pp. 606-621, 1998. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
23 | Thomas Kleymann |
Metatheory of Verification Calculi in LEGO - To what Extent Does Syntax Matter? ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop TYPES '98, Kloster Irsee, Germany, March 27-31, 1998, Selected Papers, pp. 133-148, 1998, Springer, 3-540-66537-4. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
23 | Edwin D. Mares, Paul McNamara |
Supererogation in Deontic Logic: Metatheory for DWE and Some Close Neighbours. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Stud Logica ![In: Stud Logica 59(3), pp. 397-415, 1997. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
23 | Brian Vickery |
Metatheory and information science. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Documentation ![In: J. Documentation 53(5), pp. 457-476, 1997. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
23 | David Sands 0001 |
From SOS Rules to Proof Principles: An Operational Metatheory for Functional Languages. ![Search on Bibsonomy](Pics/bibsonomy.png) |
POPL ![In: Conference Record of POPL'97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, Paris, France, 15-17 January 1997, pp. 428-441, 1997, ACM Press, 0-89791-853-3. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
23 | Fausto Giunchiglia, Paolo Traverso |
A Metatheory of a Mechanized Object Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Artif. Intell. ![In: Artif. Intell. 80(1-2), pp. 197-241, 1996. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
23 | Christos H. Papadimitriou |
Database metatheory: asking the big queries. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SIGACT News ![In: SIGACT News 26(3), pp. 13-30, 1995. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
|
23 | Christos H. Papadimitriou |
Database Metatheory: Asking the Big Queries. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PODS ![In: Proceedings of the Fourteenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, May 22-25, 1995, San Jose, California, USA, pp. 1-10, 1995, ACM Press, 0-89791-730-8. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
|
23 | Judith L. Underwood |
Tableaux for Intuitionistic Predicate Logic as Metatheory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TABLEAUX ![In: Theorem Proving with Analytic Tableaux and Related Methods, 4th International Workshop, TABLEAUX '95, Schloß Rheinfels, St. Goar, Germany, May 7-10, 1995, Proceedings, pp. 138-153, 1995, Springer, 3-540-59338-1. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
|
23 | Healfdene Goguen |
The Metatheory of UTT. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop TYPES'94, Båstad, Sweden, June 6-10, 1994, Selected Papers, pp. 60-82, 1994, Springer, 3-540-60579-7. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
23 | Alessandro Armando, Alessandro Cimatti, Luca Viganò 0001 |
Building and Executing Proof Strategies in a Formal Metatheory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AI*IA ![In: Advances in Artificial Intelligence, Third Congress of the Italian Association for Artificial Intelligence, AI*IA'93, Torino, Italy, October 26-28, 1993, Proceedings, pp. 11-22, 1993, Springer, 3-540-57292-9. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
23 | Andreas Hamfelt, Åke Hansson |
A Semiformal Metatheory for Fragmentary and Multilayered Knowledge as an Interactive Metalogic Program. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FGCS ![In: Proceedings of the International Conference on Fifth Generation Computer Systems. FGCS 1992, June 1-5, Tokyo, Japan., pp. 1107-1114, 1992, IOS Press, 90-5199-099-5. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP BibTeX RDF |
|
23 | Vladimir Lifschitz |
Toward a Metatheory of Action. ![Search on Bibsonomy](Pics/bibsonomy.png) |
KR ![In: Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning (KR'91). Cambridge, MA, USA, April 22-25, 1991., pp. 376-386, 1991, Morgan Kaufmann, 1-55860-165-1. The full citation details ...](Pics/full.jpeg) |
1991 |
DBLP BibTeX RDF |
|