Search results for "metatheory"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
71	Christian Urban, James Cheney, Stefan Berghofer	Mechanizing the Metatheory of LF.	LICS	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.	VSTTE	2005	DBLP DOI BibTeX RDF
57	Robin Adams 0001	Formalized Metatheory with Terms Represented by an Indexed Family of Types.	TYPES	2004	DBLP DOI BibTeX RDF
57	Douglas J. Howe	Computational Metatheory in Nuprl.	CADE	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.	POPL	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.	POPL	2008	DBLP DOI BibTeX RDF	locally nameless, binding, coq
40	Andreas Abel 0001, Dulma Rodriguez	Syntactic Metatheory of Higher-Order Subtyping.	CSL	2008	DBLP DOI BibTeX RDF	Higher-order subtyping, bounded quantification, algorithmic subtyping, hereditary substitution
40	James Cheney, Alberto Momigliano	Mechanized metatheory model-checking.	PPDP	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.	TPHOLs	2005	DBLP DOI BibTeX RDF
40	Fiora Pirri, Raymond Reiter	Some Contributions to the Metatheory of the Situation Calculus.	J. ACM	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.	CADE	1999	DBLP DOI BibTeX RDF
40	David A. Basin, Seán Matthews	Structuring Metatheory on Inductive Definitions.	CADE	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.	All About Maude	2007	DBLP DOI BibTeX RDF
34	Seán Matthews	A Practical Implementation of Simple Consequence Relations Using Inductive Definitions.	CADE	1997	DBLP DOI BibTeX RDF
31	Ralph L. London	Certification of algorithm 245 [M1]: treesort 3: proof of algorithms - a new kind of certification.	Commun. ACM	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.	CoRR	2024	DBLP DOI BibTeX RDF
23	Ende Jin, Nada Amin, Yizhou Zhang 0001	Extensible Metatheory Mechanization via Family Polymorphism.	Proc. ACM Program. Lang.	2023	DBLP DOI BibTeX RDF
23	Michalis Kokologiannakis, Ori Lahav 0001, Viktor Vafeiadis	Kater: Automating Weak Memory Model Metatheory and Consistency Checking.	Proc. ACM Program. Lang.	2023	DBLP DOI BibTeX RDF
23	Takahiro Yamada	Wright's Strict Finitistic Logic in the Classical Metatheory: The Propositional Case.	J. Philos. Log.	2023	DBLP DOI BibTeX RDF
23	Maristela Rocha	A Study of the Metatheory of Assertoric Syllogistic.	Logica Universalis	2023	DBLP DOI BibTeX RDF
23	Rafaël Bocquet, Ambrus Kaposi, Christian Sattler	For the Metatheory of Type Theory, Internal Sconing Is Enough.	CoRR	2023	DBLP DOI BibTeX RDF
23	Javier Díaz	Metatheory of Q0.	Arch. Formal Proofs	2023	DBLP BibTeX RDF
23	Rafaël Bocquet, Ambrus Kaposi, Christian Sattler	For the Metatheory of Type Theory, Internal Sconing Is Enough.	FSCD	2023	DBLP DOI BibTeX RDF
23	Jeremy G. Siek	The Metatheory of Gradual Typing: State of the Art and Challenges (Invited Talk).	CALCO	2023	DBLP DOI BibTeX RDF
23	Marcelo Fiore, Dmitrij Szamozvancev	Formal metatheory of second-order abstract syntax.	Proc. ACM Program. Lang.	2022	DBLP DOI BibTeX RDF
23	Guillermo Badia, Zach Weber, Patrick Girard 0004	Paraconsistent Metatheory: New Proofs with Old Tools.	J. Philos. Log.	2022	DBLP DOI BibTeX RDF
23	Frederik Krogsdal Jacobsen, Jørgen Villadsen	Teaching Functional Programmers Logic and Metatheory.	TFPIE	2022	DBLP DOI BibTeX RDF
23	Marcelo Fiore, Dmitrij Szamozvancev	Formal Metatheory of Second-Order Abstract Syntax.	CoRR	2022	DBLP BibTeX RDF
23	Jonathan Sterling	First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory.		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.	Math. Struct. Comput. Sci.	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.	Math. Struct. Comput. Sci.	2021	DBLP DOI BibTeX RDF
23	Andrew Joseph McCarthy	Modal Metatheory for Quantified Modal Logic, With and Without the Barcan Formulas.	Notre Dame J. Formal Log.	2021	DBLP DOI BibTeX RDF
23	Alessandro Cheli	Metatheory.jl: Fast and Elegant Algebraic Computation in Julia with Extensible Equality Saturation.	J. Open Source Softw.	2021	DBLP DOI BibTeX RDF
23	Fabrizio Montesi, Marco Peressotti	Linear Logic, the π-calculus, and their Metatheory: A Recipe for Proofs as Processes.	CoRR	2021	DBLP BibTeX RDF
23	Alessandro Cheli	Metatheory.jl: Fast and Elegant Algebraic Computation in Julia with Extensible Equality Saturation.	CoRR	2021	DBLP BibTeX RDF
23	Jacob Errington, Junyoung Jang 0001, Brigitte Pientka	Harpoon: Mechanizing Metatheory Interactively - (System Description).	CADE	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.	PLDI	2021	DBLP DOI BibTeX RDF
23	James Wood, Robert Atkey	A Linear Algebra Approach to Linear Metatheory.	Linearity&TLLA@IJCAR-FSCD	2020	DBLP DOI BibTeX RDF
23	Patrick Girard 0004, Zach Weber	Modal Logic without Contraction in a Metatheory without Contraction.	Rev. Symb. Log.	2019	DBLP DOI BibTeX RDF
23	Dale Miller 0001	Mechanized Metatheory Revisited.	J. Autom. Reason.	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.	J. Autom. Reason.	2019	DBLP DOI BibTeX RDF
23	Jasmin Christian Blanchette	Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk).	CPP	2019	DBLP DOI BibTeX RDF
23	Megan Katsumi, Michael Grüninger	The metatheory of ontology reuse.	Appl. Ontology	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.	Cogn. Sci.	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.	CoRR	2018	DBLP BibTeX RDF
23	Georg Schiemer, Richard Zach, Erich H. Reck	Carnap's early metatheory: scope and limits.	Synth.	2017	DBLP DOI BibTeX RDF
23	Ernesto Copello, Nora Szasz, Alvaro Tasistro	Formal metatheory of the Lambda calculus using Stoughton's substitution.	Theor. Comput. Sci.	2017	DBLP DOI BibTeX RDF
23	James Cheney, Alberto Momigliano	αCheck: A mechanized metatheory model-checker.	CoRR	2017	DBLP BibTeX RDF
23	Michael Rawson	Verified Metatheory and Type Inference for a Name-Carrying Simply-Typed Lambda Calculus.	Arch. Formal Proofs	2017	DBLP BibTeX RDF
23	James Cheney, Alberto Momigliano	αCheck: A mechanized metatheory model checker.	Theory Pract. Log. Program.	2017	DBLP DOI BibTeX RDF
23	Dale Miller 0001	Mechanized Metatheory Revisited: An Extended Abstract (Invited Paper).	TYPES	2016	DBLP DOI BibTeX RDF
23	David Darais, David Van Horn	Constructive Galois connections: taming the Galois connection framework for mechanized metatheory.	ICFP	2016	DBLP DOI BibTeX RDF
23	Christian Doczkal	A machine-checked constructive metatheory of computation tree logic.		2016	RDF
23	Omar Alaqeeli	The metatheory of the monadic hybrid calculus.		2016	RDF
23	Albert Meijer 0001, Victor Bekkers	A metatheory of e-government: Creating some order in a fragmented research field.	Gov. Inf. Q.	2015	DBLP DOI BibTeX RDF
23	David Darais, David Van Horn	Constructive Galois Connections: Taming the Galois Connection Framework for Mechanized Metatheory.	CoRR	2015	DBLP BibTeX RDF
23	David Darais, Matthew Might, David Van Horn	Galois transformers and modular abstract interpreters: reusable metatheory for program analysis.	OOPSLA	2015	DBLP DOI BibTeX RDF
23	Kaustuv Chaudhuri, Matteo Cimini, Dale Miller 0001	A Lightweight Formalization of the Metatheory of Bisimulation-Up-To.	CPP	2015	DBLP DOI BibTeX RDF
23	Peter Johan Lor	Revitalizing comparative library and information science: theory and metatheory.	J. Documentation	2014	DBLP DOI BibTeX RDF
23	Leon James, Diane Nahl	A metatheory integrating social, biological and technological factors in information behavior research.	Webology	2014	DBLP BibTeX RDF
23	Jonghyun Park, Jeongbong Seo, Sungwoo Park, Gyesik Lee	Mechanizing Metatheory Without Typing Contexts.	J. Autom. Reason.	2014	DBLP DOI BibTeX RDF
23	Rodrigo Geraldo Ribeiro, Lucília Figueiredo, Carlos Camarão 0001	Mechanized metatheory for a λ-calculus with trust types.	J. Braz. Comput. Soc.	2013	DBLP DOI BibTeX RDF
23	Andrew Bacon	Non-classical Metatheory for Non-classical Logics.	J. Philos. Log.	2013	DBLP DOI BibTeX RDF
23	Andreas Schropp, Andrei Popescu 0001	Nonfree Datatypes in Isabelle/HOL - Animating a Many-Sorted Metatheory.	CPP	2013	DBLP DOI BibTeX RDF
23	Jasmin Christian Blanchette, Andrei Popescu 0001	Mechanizing the Metatheory of Sledgehammer.	FroCos	2013	DBLP DOI BibTeX RDF
23	Kim G. Larsen, Radu Mardare, Claus R. Thrane	Parameterized Metatheory for Continuous Markovian Logic	QFM	2012	DBLP DOI BibTeX RDF
23	Radu Mardare, Luca Cardelli, Kim G. Larsen	Continuous Markovian Logics - Axiomatization and Quantified Metatheory	Log. Methods Comput. Sci.	2012	DBLP DOI BibTeX RDF
23	Andrew W. Appel, Robert Dockins, Xavier Leroy	A List-Machine Benchmark for Mechanized Metatheory.	J. Autom. Reason.	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.	J. Autom. Reason.	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.	ESOP	2012	DBLP DOI BibTeX RDF
23	Victor Raskin	A Little Metatheory: Thought on What aTheory of Computational Humor Should Look Like.	AAAI Fall Symposium: Artificial Intelligence of Humor	2012	DBLP BibTeX RDF
23	Christian Urban, James Cheney, Stefan Berghofer	Mechanizing the metatheory of LF.	ACM Trans. Comput. Log.	2011	DBLP DOI BibTeX RDF
23	Robert E. Kent	The Information Flow Framework: A Descriptive Category Metatheory	CoRR	2011	DBLP BibTeX RDF
23	James Cheney, Christian Urban	Mechanizing the Metatheory of mini-XQuery.	CPP	2011	DBLP DOI BibTeX RDF
23	Wilmer Ricciotti	Theoretical and implementation aspects in the mechanization of the metatheory of programming languages.		2011	RDF
23	Patricia Johann, Alex Simpson, Janis Voigtländer	A Generic Operational Metatheory for Algebraic Effects.	LICS	2010	DBLP DOI BibTeX RDF
23	Christian Urban, James Cheney, Stefan Berghofer	Mechanizing the Metatheory of LF	CoRR	2008	DBLP BibTeX RDF
23	Andreas Herzig, Ivan José Varzinczak	Metatheory of actions: Beyond consistency.	Artif. Intell.	2007	DBLP DOI BibTeX RDF
23	Robert Harper 0001, Daniel R. Licata	Mechanizing metatheory in a logical framework.	J. Funct. Program.	2007	DBLP DOI BibTeX RDF
23	Andrew W. Appel, Xavier Leroy	A List-machine Benchmark for Mechanized Metatheory: (Extended Abstract).	LFMTP@FLoC	2006	DBLP DOI BibTeX RDF
23	Andreas Herzig, Ivan José Varzinczak	Metatheory of actions: beyond consistency	CoRR	2006	DBLP BibTeX RDF
23	Miroljub Dugic, Milan M. Cirkovic, Dejan Rakovic	On a Possible Physical Metatheory of Consciousness.	Open Syst. Inf. Dyn.	2002	DBLP DOI BibTeX RDF
23	Joseph Vanderwaart, Karl Crary	A Simplified Account of the Metatheory of Linear LF.	LFM	2002	DBLP DOI BibTeX RDF
23	David A. Basin, Seán Matthews	Structuring Metatheory on Inductive Definitions.	Inf. Comput.	2000	DBLP DOI BibTeX RDF
23	Brenda Dervin	On studying information seeking methodologically: the implications of connecting metatheory to method.	Inf. Process. Manag.	1999	DBLP DOI BibTeX RDF
23	Erik Sandewall	Cognitive Robotics Logic and its Metatheory: Features and Fluents Revisited.	Electron. Trans. Artif. Intell.	1998	DBLP BibTeX RDF
23	Alessandro Armando, Jason Gallagher, Alan Smaill, Alan Bundy	Automating the Synthesis of Decision Procedures in a Constructive Metatheory.	Ann. Math. Artif. Intell.	1998	DBLP DOI BibTeX RDF
23	Birger Hjørland	Theory and metatheory of information science: a new interpretation.	J. Documentation	1998	DBLP DOI BibTeX RDF
23	Thomas Kleymann	Metatheory of Verification Calculi in LEGO - To what Extent Does Syntax Matter?	TYPES	1998	DBLP DOI BibTeX RDF
23	Edwin D. Mares, Paul McNamara	Supererogation in Deontic Logic: Metatheory for DWE and Some Close Neighbours.	Stud Logica	1997	DBLP DOI BibTeX RDF
23	Brian Vickery	Metatheory and information science.	J. Documentation	1997	DBLP DOI BibTeX RDF
23	David Sands 0001	From SOS Rules to Proof Principles: An Operational Metatheory for Functional Languages.	POPL	1997	DBLP DOI BibTeX RDF
23	Fausto Giunchiglia, Paolo Traverso	A Metatheory of a Mechanized Object Theory.	Artif. Intell.	1996	DBLP DOI BibTeX RDF
23	Christos H. Papadimitriou	Database metatheory: asking the big queries.	SIGACT News	1995	DBLP DOI BibTeX RDF
23	Christos H. Papadimitriou	Database Metatheory: Asking the Big Queries.	PODS	1995	DBLP DOI BibTeX RDF
23	Judith L. Underwood	Tableaux for Intuitionistic Predicate Logic as Metatheory.	TABLEAUX	1995	DBLP DOI BibTeX RDF
23	Healfdene Goguen	The Metatheory of UTT.	TYPES	1994	DBLP DOI BibTeX RDF
23	Alessandro Armando, Alessandro Cimatti, Luca Viganò 0001	Building and Executing Proof Strategies in a Formal Metatheory.	AI*IA	1993	DBLP DOI BibTeX RDF
23	Andreas Hamfelt, Åke Hansson	A Semiformal Metatheory for Fragmentary and Multilayered Knowledge as an Interactive Metalogic Program.	FGCS	1992	DBLP BibTeX RDF
23	Vladimir Lifschitz	Toward a Metatheory of Action.	KR	1991	DBLP BibTeX RDF