[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
A research grant position for one year in the field of Computer Aided Formal
Reasoning is available at the University of Udine (Dept. of Mathematics,
Computer Science and Physics). The research program is about the development of
the core of a proof assistant based on LFP [1-6], a logical framework allowing
to make calls to external oracles (e.g., other logical frameworks, decision
methods etc.), starting from an existing type checker written in OCaml.
APPLICATION DEADLINE 07/09/2018 23:59 - Europe/Brussels
Further details:
https://euraxess.ec.europa.eu/jobs/330711
Notice of competition:
http://web.uniud.it/ateneo/normativa/albo_ufficiale/660%20-%202018/20180660.2%20Notice%20-%20ARIC.pdf
References
[1] F. Honsell, L. Liquori, P. Maksimovic and I. Scagnetto. Plugging-in proof
development environments using Locks in LF. In Mathematical Structures in
Computer Science, 1-28, 2018. doi:10.1017/S0960129518000105 [2] F. Honsell, L.
Liquori, P. Maksimovic and I. Scagnetto. LLFP: A Logical Framework for Modeling
External Evidence, Side Conditions, and Proof Irrelevance using Monads. In
lmcs:3771 - Logical Methods in Computer Science, July 6, 2017, Volume 13, Issue
3.
[3] F. Honsell, M. Lenisa, L. Liquori, P. Maksimovic and I. Scagnetto. An Open
Logical Framework. Journal of Logic and Computation (2016) 26 (1): 293-335.
[4] F. Honsell, L. Liquori, P. Maksimovic and I. Scagnetto. Gluing together
Proof Environments: Canonical extensions of LF Type Theories featuring Locks.
In Proc. of LFMTP 2015 (Logical Frameworks and Meta-Languages: Theory and
Practice, Affiliated with CADE-25), Berlin, Germany, 01/08/2015, pp. 3--17,
http://dx.doi.org/10.4204/EPTCS.185.1, ISSN: 2075-2180, Open Publishing
Association.
[5] F. Honsell, L. Liquori and I. Scagnetto. LaxF: Side Conditions and External
Evidence as Monads. In Proc. of MFCS 2014 (39th International Symposium on
Mathematical Foundations of Computer Science), Part I, Budapest, Hungary,
25-29/08/2014, Lecture Notes in Computer Science, Vol. 8634, pages 327-339,
Springer, ISBN 978-3-662-44521-1.
[6] F. Honsell, M. Lenisa, L. Liquori, P. Maksimovic and I. Scagnetto. LFP - A
Logical Framework with External Predicates. In Proc. of LFMTP 2012 (7th
International Workshop on Logical Frameworks and Meta-languages:
Theory and Practice), Copenhagen, Denmark - September 9, 2012.
