{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:54:21Z","timestamp":1770288861933,"version":"3.49.0"},"reference-count":33,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,3,2]],"date-time":"2012-03-02T00:00:00Z","timestamp":1330646400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>The paper describes the refinement algorithm for the Calculus of (Co)Inductive Constructions (CIC) implemented in the interactive theorem prover Matita. The refinement algorithm is in charge of giving a meaning to the terms, types and proof terms directly written by the user or generated by using tactics, decision procedures or general automation. The terms are written in an \"external syntax\" meant to be user friendly that allows omission of information, untyped binders and a certain liberal use of user defined sub-typing. The refiner modifies the terms to obtain related well typed terms in the internal syntax understood by the kernel of the ITP. In particular, it acts as a type inference algorithm when all the binders are untyped. The proposed algorithm is bi-directional: given a term in external syntax and a type expected for the term, it propagates as much typing information as possible towards the leaves of the term. Traditional mono-directional algorithms, instead, proceed in a bottom-up way by inferring the type of a sub-term and comparing (unifying) it with the type expected by its context only at the end. We propose some novel bi-directional rules for CIC that are particularly effective. Among the benefits of bi-directionality we have better error message reporting and better inference of dependent types. Moreover, thanks to bi-directionality, the coercion system for sub-typing is more effective and type inference generates simpler unification problems that are more likely to be solved by the inherently incomplete higher order unification algorithms implemented. Finally we introduce in the external syntax the notion of vector of placeholders that enables to omit at once an arbitrary number of arguments. Vectors of placeholders allow a trivial implementation of implicit arguments and greatly simplify the implementation of primitive and simple tactics.<\/jats:p>","DOI":"10.2168\/lmcs-8(1:18)2012","type":"journal-article","created":{"date-parts":[[2012,9,6]],"date-time":"2012-09-06T10:03:11Z","timestamp":1346925791000},"source":"Crossref","is-referenced-by-count":11,"title":["A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions"],"prefix":"10.46298","volume":"Volume 8, Issue 1","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9677-6350","authenticated-orcid":false,"given":"Andrea","family":"Asperti","sequence":"first","affiliation":[]},{"given":"Wilmer","family":"Ricciotti","sequence":"additional","affiliation":[]},{"given":"Claudio Sacerdoti","family":"Coen","sequence":"additional","affiliation":[]},{"given":"Enrico","family":"Tassi","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,3,2]]},"reference":[{"key":"10.2168\/LMCS-8(1:18)2012_armentano","first-page":"1","volume":"1","author":"Andrea Asperti and Cristian Armentano","year":"2008","journal-title":"Journal of Formalized Reasoning"},{"key":"10.2168\/LMCS-8(1:18)2012_asperti-ricciotti","doi-asserted-by":"crossref","unstructured":"Andrea Asperti and Wilmer Ricciotti. About the formalization of some results by Chebyshev in number theory. InProc. of TYPES'08, volume 5497 ofLNCS, pages 19-31. Springer-Verlag, 2009.","DOI":"10.1007\/978-3-642-02444-3_2"},{"key":"10.2168\/LMCS-8(1:18)2012_matitapoplmark","doi-asserted-by":"crossref","unstructured":"Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi. Formal metatheory of programming languages in the Matita interactive theorem prover.Journal of Automated Reasoning: Special Issue on the Poplmark Challenge. Published online, May 2011.","DOI":"10.1007\/s10817-011-9228-z"},{"issue":"1","key":"10.2168\/LMCS-8(1:18)2012_ck-sadhana","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1007\/s12046-009-0003-3","volume":"34","author":"Andrea Asperti, Wilmer Ricciotti, Claudi","year":"2009","journal-title":"Sadhana"},{"key":"10.2168\/LMCS-8(1:18)2012_unification-hints","doi-asserted-by":"crossref","unstructured":"Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi. Hints in unification. InTPHOLs 2009, volume 5674\/2009 ofLNCS, pages 84-98. Springer-Verlag, 2009.","DOI":"10.1007\/978-3-642-03359-9_8"},{"issue":"2","key":"10.2168\/LMCS-8(1:18)2012_matita-jar-uitp","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/s10817-007-9070-5","volume":"39","author":"Andrea Asperti, Claudio Sacerdoti Coen,","year":"2007","journal-title":"Journal of Automated Reasoning"},{"key":"10.2168\/LMCS-8(1:18)2012_BarendregtH:lawcwt","doi-asserted-by":"crossref","unstructured":"Henk Barendregt. Lambda Calculi with Types. In Abramsky, Samson and others, editor,Handbook of Logic in Computer Science, volume 2. Oxford University Press, 1992.","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"10.2168\/LMCS-8(1:18)2012_agda","doi-asserted-by":"crossref","unstructured":"Ana Bove, Peter Dybjer, and Ulf Norell. A brief overview of Agda - a functional language with dependent types. InTheorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, volume 5674 ofLNCS, pages 73-78. Springer, 2009.","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"10.2168\/LMCS-8(1:18)2012_callaghan00coherence","unstructured":"P. Callaghan. Coherence checking of coercions in Plastic. InIn Proc. Workshop on Subtyping and Dependent Types in Programming, 2000."},{"key":"10.2168\/LMCS-8(1:18)2012_chenPHD","unstructured":"Gang Chen.Subtyping, Type Conversion and Transitivity Elimination. PhD thesis, University Paris 7, 1998."},{"key":"10.2168\/LMCS-8(1:18)2012_TS11","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1017\/S0960129510000320","volume":"21","author":"Claudio Sacerdoti Coen and Enrico Tassi","year":"2011","journal-title":"Mathematical Structures in Computer Science"},{"key":"10.2168\/LMCS-8(1:18)2012_coq","doi-asserted-by":"crossref","unstructured":"The Coq proof-assistant., 2009. Thierry Coquand and G\u00e9rard P. Huet. The Calculus of Constructions.Inf. Comput., 76(2\/3):95-120, 1988.","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"10.2168\/LMCS-8(1:18)2012_dunfieldgreedy","doi-asserted-by":"crossref","unstructured":"Joshua Dunfield. Greedy bidirectional polymorphism. InML Workshop (ML '09), pages 15-26, August 2009. http:\/\/www.cs.cmu.edu\/ joshuad\/papers\/poly\/.","DOI":"10.1145\/1596627.1596631"},{"key":"10.2168\/LMCS-8(1:18)2012_pfenning3","doi-asserted-by":"crossref","unstructured":"Joshua Dunfield and Frank Pfenning. Tridirectional typechecking. In X. Leroy, editor,Conference Record of the 31st Annual Symposium on Principles of Programming Languages (POPL'04), pages 281-292, 2004.","DOI":"10.1145\/964001.964025"},{"key":"10.2168\/LMCS-8(1:18)2012_canonical-structures","doi-asserted-by":"crossref","unstructured":"Francois Garillot, Georges Gonthier, Assia Mahboubi, and Laurence Rideau. Packaging mathematical structures. InProceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs '09, pages 327-342, Berlin, Heidelberg, 2009. Springer-Verlag.","DOI":"10.1007\/978-3-642-03359-9_23"},{"issue":"1","key":"10.2168\/LMCS-8(1:18)2012_huet2order","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G\u00e9rard P. Huet","year":"1975","journal-title":"Theor. Comput. Sci."},{"key":"10.2168\/LMCS-8(1:18)2012_isabelle","unstructured":"The Isabelle proof-assistant. http:\/\/www.cl.cam.ac.uk\/Research\/HVG\/Isabelle\/. The Lego proof-assistant. http:\/\/www.dcs.ed.ac.uk\/home\/lego\/."},{"issue":"1","key":"10.2168\/LMCS-8(1:18)2012_coercivesubtyping","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1093\/logcom\/9.1.105","volume":"9","author":"Zhaohui Luo","year":"1999","journal-title":"J. Logic and Computation"},{"key":"10.2168\/LMCS-8(1:18)2012_munoz","unstructured":"C\u00e9sar Mu\u00f1oz.A Calculus of Substitutions for Incomplete-Proof Representation in Type Theory. PhD thesis, INRIA, November 1997."},{"key":"10.2168\/LMCS-8(1:18)2012_phd-norell","unstructured":"Ulf Norell.Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 G\u00f6teborg, Sweden, September 2007."},{"key":"10.2168\/LMCS-8(1:18)2012_mohring","unstructured":"Christine Paulin-Mohring.D\u00e9finitions Inductives en Th\u00e9orie des Types d'Ordre Sup\u00e9rieur. Habilitation \u00e0 diriger les recherches, Universit\u00e9 Claude Bernard Lyon I, December 1996."},{"key":"10.2168\/LMCS-8(1:18)2012_piercelocaltype","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/345099.345100","volume":"22","author":"Benjamin C. Pierce and David N. Turner","year":"2000","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10.2168\/LMCS-8(1:18)2012_pollackFAC02","doi-asserted-by":"crossref","first-page":"386","DOI":"10.1007\/s001650200018","volume":"13","author":"Robert Pollack","year":"2002","journal-title":"Formal Aspects of Computing"},{"key":"10.2168\/LMCS-8(1:18)2012_csc-phd","unstructured":"Claudio Sacerdoti Coen.Mathematical Knowledge Management and Interactive Theorem Proving. PhD thesis, University of Bologna, 2004. Technical Report UBLCS 2004-5."},{"key":"10.2168\/LMCS-8(1:18)2012_mcs2008","first-page":"355","volume":"2","author":"Claudio Sacerdoti Coen and Stefano Zacch","year":"2008","journal-title":"Journal of Mathematics in Computer Science, special issue on Management of Mathematical Knowledge"},{"key":"10.2168\/LMCS-8(1:18)2012_saibi-inheritance","doi-asserted-by":"crossref","unstructured":"Amokrane Sa\u00efbi. Typing algorithm in type theory with inheritance. InProceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL '97, pages 292-301, New York, NY, USA, 1997. ACM.","DOI":"10.1145\/263699.263742"},{"key":"10.2168\/LMCS-8(1:18)2012_russell","doi-asserted-by":"crossref","unstructured":"Matthieu Sozeau. Subset coercions in Coq. InTypes for Proofs and Programs, volume 4502\/2007 ofLNCS, pages 237-252. Springer-Verlag, 2006.","DOI":"10.1007\/978-3-540-74464-1_16"},{"key":"10.2168\/LMCS-8(1:18)2012_SozeauO08","doi-asserted-by":"crossref","unstructured":"Matthieu Sozeau and Nicolas Oury. First-class type classes. InProceedings of TPHOLs, pages 278-293, 2008.","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"10.2168\/LMCS-8(1:18)2012_Spiwack","unstructured":"Arnaud Spiwack.Verified Computing in Homological Algebra. A Journey Esploring the Power and Limits of Dependent Type Theory. PhD thesis, \u00c9cole Polytechniqe, 2011."},{"key":"10.2168\/LMCS-8(1:18)2012_strecker","unstructured":"Martin Strecker.Construction and Deduction in Type Theories. PhD thesis, Universit\u00e4t Ulm, 1998."},{"key":"10.2168\/LMCS-8(1:18)2012_StuckeySW06","doi-asserted-by":"crossref","unstructured":"Peter J. Stuckey, Martin Sulzmann, and Jeremy Wazny. Type processing by constraint reasoning. InAPLAS, pages 1-25, 2006.","DOI":"10.1007\/11924661_1"},{"key":"10.2168\/LMCS-8(1:18)2012_tassi-phd","unstructured":"Enrico Tassi.Interactive Theorem Provers: issues faced as a user and tackled as a developer. PhD thesis, University of Bologna, 2008."},{"key":"10.2168\/LMCS-8(1:18)2012_Werner","unstructured":"Benjamin Werner.Une Th\u00e9orie des Constructions Inductives. PhD thesis, Universit\u00e9 Paris VII, May 1994."}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1044\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1044\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,28]],"date-time":"2024-04-28T23:53:06Z","timestamp":1714348386000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1044"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,3,2]]},"references-count":33,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(1:18)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1202.4905","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1202.4905","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,3,2]]},"article-number":"1044"}}