Edit Profile (opens in new tab) Momigliano, Alberto Compute Distance To: Compute Author ID: momigliano.alberto Published as: Momigliano, Alberto; Momigliano, A. External Links: MGP · ORCID Documents Indexed: 25 Publications since 1992 3 Contributions as Editor Co-Authors: 25 Co-Authors with 26 Joint Publications 379 Co-Co-Authors all top 5 Co-Authors 2 single-authored 5 Fiorentini, Camillo 5 Ornaghi, Mario 5 Pientka, Brigitte 4 Ambler, Simon J. 4 Felty, Amy P. 3 Beringer, Lennart 3 Crole, Roy L. 3 Hofmann, Martin 2 Aspinall, David 2 Ferrari, Mauro 2 Loidl, Hans-Wolfgang 2 Tiu, Alwen Fernanto 1 Abel, Andreas M. 1 Allais, Guillaume 1 Avellone, Alessandro 1 Cheney, James 1 Hameer, Aliya 1 Lau, Kung-Kiu 1 Martin, Alan J. 1 Pettorossi, Alberto 1 Pfenning, Frank 1 Schäfer, Steven 1 Shkaravska, Olha 1 Stark, Kathrin 1 Thibodeau, David all top 5 Serials 3 Fundamenta Informaticae 2 Journal of Automated Reasoning 2 MSCS. Mathematical Structures in Computer Science 2 Electronic Notes in Theoretical Computer Science 1 Theoretical Computer Science 1 Journal of Logic and Computation 1 Journal of Functional Programming 1 Theory and Practice of Logic Programming 1 ACM Transactions on Computational Logic 1 Journal of Applied Logic Fields 26 Computer science (68-XX) 17 Mathematical logic and foundations (03-XX) 3 General and overarching topics; collections (00-XX) 1 History and biography (01-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 19 Publications have been cited 104 times in 62 Documents Cited by ▼ Year ▼ Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax. Zbl 1252.68252Felty, Amy; Momigliano, Alberto 17 2012 Induction and co-induction in sequent calculus. Zbl 1100.03516Momigliano, Alberto; Tiu, Alwen 12 2004 The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey. Zbl 1357.68198Felty, Amy P.; Momigliano, Alberto; Pientka, Brigitte 11 2015 Automatic certification of heap consumption. Zbl 1108.68374Beringer, Lennart; Hofmann, Martin; Momigliano, Alberto; Shkaravska, Olha 9 2005 A program logic for resources. Zbl 1133.68010Aspinall, David; Beringer, Lennart; Hofmann, Martin; Loidl, Hans-Wolfgang; Momigliano, Alberto 8 2007 Combining higher order abstract syntax with tactical theorem proving and (co)induction. Zbl 1013.68545Ambler, Simon J.; Crole, Roy L.; Momigliano, Alberto 7 2002 Cut elimination for a logic with induction and co-induction. Zbl 1278.03086Tiu, Alwen; Momigliano, Alberto 7 2012 Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions. Zbl 1400.68194Felty, Amy; Momigliano, Alberto; Pientka, Brigitte 4 2018 Elimination of negation in a logical framework. Zbl 0973.68039Momigliano, Alberto 4 2000 POPLMark reloaded: mechanizing proofs by logical relations. Zbl 1442.68257Abel, Andreas; Allais, Guillaume; Hameer, Aliya; Pientka, Brigitte; Momigliano, Alberto; Schäfer, Steven; Stark, Kathrin 4 2019 Multi-level meta-reasoning with higher-order abstract syntax. Zbl 1029.68043Momigliano, Alberto; Ambler, Simon J. 4 2003 \(\alpha\mathrm{Check}\): a mechanized metatheory model checker. Zbl 1379.68236Cheney, James; Momigliano, Alberto 4 2017 A case study in programming coinductive proofs: Howe’s method. Zbl 1430.68418Momigliano, Alberto; Pientka, Brigitte; Thibodeau, David 3 2019 A hybrid encoding of Howe’s method for establishing congruence of bisimilarity. Zbl 1270.68072Momigliano, Alberto; Ambler, Simon J.; Crole, Roy L. 3 2002 Higher-order pattern complement and the strict \(\lambda\)-calculus. Zbl 1365.68155Momigliano, Alberto; Pfenning, Frank 2 2003 A program logic for resource verification. Zbl 1099.68584Aspinall, David; Beringer, Lennart; Hofmann, Martin; Loidl, Hans-Wolfgang; Momigliano, Alberto 2 2004 Minimal negation and hereditary Harrop formulae. Zbl 0977.68513Momigliano, Alberto 1 1992 Two-level hybrid: a system for reasoning using higher-order abstract syntax. Zbl 1278.03062Momigliano, Alberto; Martin, Alan J.; Felty, Amy P. 1 2008 Snapshot generation in a constructive object-oriented modeling language. Zbl 1179.68029Ferrari, Mauro; Fiorentini, Camillo; Momigliano, Alberto; Ornaghi, Mario 1 2008 POPLMark reloaded: mechanizing proofs by logical relations. Zbl 1442.68257Abel, Andreas; Allais, Guillaume; Hameer, Aliya; Pientka, Brigitte; Momigliano, Alberto; Schäfer, Steven; Stark, Kathrin 4 2019 A case study in programming coinductive proofs: Howe’s method. Zbl 1430.68418Momigliano, Alberto; Pientka, Brigitte; Thibodeau, David 3 2019 Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions. Zbl 1400.68194Felty, Amy; Momigliano, Alberto; Pientka, Brigitte 4 2018 \(\alpha\mathrm{Check}\): a mechanized metatheory model checker. Zbl 1379.68236Cheney, James; Momigliano, Alberto 4 2017 The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey. Zbl 1357.68198Felty, Amy P.; Momigliano, Alberto; Pientka, Brigitte 11 2015 Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax. Zbl 1252.68252Felty, Amy; Momigliano, Alberto 17 2012 Cut elimination for a logic with induction and co-induction. Zbl 1278.03086Tiu, Alwen; Momigliano, Alberto 7 2012 Two-level hybrid: a system for reasoning using higher-order abstract syntax. Zbl 1278.03062Momigliano, Alberto; Martin, Alan J.; Felty, Amy P. 1 2008 Snapshot generation in a constructive object-oriented modeling language. Zbl 1179.68029Ferrari, Mauro; Fiorentini, Camillo; Momigliano, Alberto; Ornaghi, Mario 1 2008 A program logic for resources. Zbl 1133.68010Aspinall, David; Beringer, Lennart; Hofmann, Martin; Loidl, Hans-Wolfgang; Momigliano, Alberto 8 2007 Automatic certification of heap consumption. Zbl 1108.68374Beringer, Lennart; Hofmann, Martin; Momigliano, Alberto; Shkaravska, Olha 9 2005 Induction and co-induction in sequent calculus. Zbl 1100.03516Momigliano, Alberto; Tiu, Alwen 12 2004 A program logic for resource verification. Zbl 1099.68584Aspinall, David; Beringer, Lennart; Hofmann, Martin; Loidl, Hans-Wolfgang; Momigliano, Alberto 2 2004 Multi-level meta-reasoning with higher-order abstract syntax. Zbl 1029.68043Momigliano, Alberto; Ambler, Simon J. 4 2003 Higher-order pattern complement and the strict \(\lambda\)-calculus. Zbl 1365.68155Momigliano, Alberto; Pfenning, Frank 2 2003 Combining higher order abstract syntax with tactical theorem proving and (co)induction. Zbl 1013.68545Ambler, Simon J.; Crole, Roy L.; Momigliano, Alberto 7 2002 A hybrid encoding of Howe’s method for establishing congruence of bisimilarity. Zbl 1270.68072Momigliano, Alberto; Ambler, Simon J.; Crole, Roy L. 3 2002 Elimination of negation in a logical framework. Zbl 0973.68039Momigliano, Alberto 4 2000 Minimal negation and hereditary Harrop formulae. Zbl 0977.68513Momigliano, Alberto 1 1992 all cited Publications top 5 cited Publications all top 5 Cited by 106 Authors 9 Pientka, Brigitte 8 Momigliano, Alberto 6 Felty, Amy P. 6 Miller, Dale Allen 5 Beringer, Lennart 2 Allais, Guillaume 2 Aspinall, David 2 Gacek, Andrew 2 Heath, Quentin 2 Hofmann, Martin 2 Mahmoud, Mohamed Yousri 2 Montenegro, Manuel 2 Nadathur, Gopalan 2 Olarte, Carlos 2 Peña, Ricardo 2 Saabas, Ando 2 Segura, Clara 2 Szasz, Nora 2 Tasistro, Alvaro 2 Tiu, Alwen Fernanto 2 Uustalu, Tarmo 2 Xavier, Bruno 1 Abel, Andreas M. 1 Ahn, Ki Yung 1 Ambal, Guillaume 1 Aranda-López, Gabriel 1 Atkey, Robert 1 Ayala-Rincón, Mauricio 1 Baelde, David 1 Besson, Frédéric 1 Brünnler, Kai 1 Cachera, David 1 Cave, Andrew 1 Chapman, James T. E. 1 Charguéraud, Arthur 1 Cheney, James 1 Ciaffaglione, Alberto 1 Cirstea, Horatiu 1 Cohen, Liron 1 Copello, Ernesto 1 Cristiá, Maximiliano 1 Crole, Roy L. 1 Dagnino, Francesco 1 Dockins, Robert 1 Dunfield, Joshua 1 Errington, Jacob 1 Fernández, Maribel 1 Ferrari, Mauro 1 Ferreira, Francisco H. G. 1 Fiorentini, Camillo 1 Fiorino, Guido 1 Furniss, Amy 1 Gheri, Lorenzo 1 Hähnle, Reiner 1 Hainry, Emmanuel 1 Hameer, Aliya 1 Hobor, Aquinas 1 Horne, Ross 1 Jang, Junyoung 1 Jobin, Arnaud 1 Kaiser, Jonas Pilgaard 1 Kimura, Daisuke 1 Kirchner, Claude 1 Kopetz, Radu 1 Kutz, Yunus D. K. 1 Lenglet, Sergueï 1 Liquori, Luigi 1 Loidl, Hans-Wolfgang 1 Maier, Patrick 1 McBride, Conor Thomas 1 McKinna, James 1 Miculan, Marino 1 Moreau, Pierre-Etienne 1 Nieva, Susana 1 Nigam, Vivek 1 Norrish, Michael 1 Pan, Jing 1 Pavlova, Mariela 1 Péchoux, Romain 1 Pichardie, David 1 Popescu, Andrei 1 Pottier, François 1 Reis, Giselle 1 Rossi, Gianfranco 1 Roşu, Grigore 1 Rümmer, Philipp 1 Sáenz-Pérez, Fernando 1 Sánchez-Hernández, Jaime 1 Sarnat, Jeffrey 1 Schäfer, Steven 1 Schmidt-Schauß, Manfred 1 Schmitt, Alan 1 Schürmann, Carsten 1 Smolka, Gert 1 Snow, Zachary 1 Sobrinho, Daniele Nantes 1 Sotin, Pascal 1 Stark, Ian 1 Stark, Kathrin 1 Studer, Thomas ...and 6 more Authors all top 5 Cited in 13 Serials 13 Journal of Automated Reasoning 6 MSCS. Mathematical Structures in Computer Science 4 Theoretical Computer Science 4 The Journal of Logic and Algebraic Programming 3 Information and Computation 3 Logical Methods in Computer Science 2 Journal of Functional Programming 1 Annals of Pure and Applied Logic 1 Journal of Symbolic Computation 1 Annals of Mathematics and Artificial Intelligence 1 Higher-Order and Symbolic Computation 1 Theory and Practice of Logic Programming 1 Journal of Applied Logic Cited in 4 Fields 57 Computer science (68-XX) 40 Mathematical logic and foundations (03-XX) 2 Quantum theory (81-XX) 1 Order, lattices, ordered algebraic structures (06-XX) Citations by Year